Theorem spwval2 8649

Description: Value of supremum under a weak ordering. Read R sup_w A as "the R -supremum of A." ∪∪R is the field of a relation R by relfld 3521. Unlike df-sup 4583 for strong orderings, the supremum exists iff R sup_w A belongs to the field.

Hypotheses

Ref	Expression
spwval2.1	⊢ X = ∪∪R
spwval2.2	⊢ Z = {x ∈ X∣(∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))}

Assertion

Ref	Expression
spwval2	⊢ ((R ∈ U ⋀ A ∈ W) → (R supw A) = if(Z ≠ ∅, ∪Z, ℘∪X))

Distinct variable groups:   x,y,z,A   x,R,y,z   x,X,y

Proof of Theorem spwval2

Step	Hyp	Ref	Expression
1		ifcl 2384	. . . . 5 ⊢ ((∪Z ∈ V ⋀ ℘∪X ∈ V) → if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V)
2	1	ancoms 438	. . . 4 ⊢ ((℘∪X ∈ V ⋀ ∪Z ∈ V) → if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V)
3		uniexg 2877	. . . . . . . 8 ⊢ (R ∈ U → ∪R ∈ V)
4		uniexg 2877	. . . . . . . 8 ⊢ (∪R ∈ V → ∪∪R ∈ V)
5	3, 4	syl 10	. . . . . . 7 ⊢ (R ∈ U → ∪∪R ∈ V)
6		spwval2.1	. . . . . . 7 ⊢ X = ∪∪R
7	5, 6	syl5eqel 1555	. . . . . 6 ⊢ (R ∈ U → X ∈ V)
8		uniexg 2877	. . . . . 6 ⊢ (X ∈ V → ∪X ∈ V)
9	7, 8	syl 10	. . . . 5 ⊢ (R ∈ U → ∪X ∈ V)
10		pwexg 2752	. . . . 5 ⊢ (∪X ∈ V → ℘∪X ∈ V)
11	9, 10	syl 10	. . . 4 ⊢ (R ∈ U → ℘∪X ∈ V)
12		rabexg 2729	. . . . . . 7 ⊢ (X ∈ V → {x ∈ X∣(∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))} ∈ V)
13	7, 12	syl 10	. . . . . 6 ⊢ (R ∈ U → {x ∈ X∣(∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))} ∈ V)
14		spwval2.2	. . . . . 6 ⊢ Z = {x ∈ X∣(∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))}
15	13, 14	syl5eqel 1555	. . . . 5 ⊢ (R ∈ U → Z ∈ V)
16		uniexg 2877	. . . . 5 ⊢ (Z ∈ V → ∪Z ∈ V)
17	15, 16	syl 10	. . . 4 ⊢ (R ∈ U → ∪Z ∈ V)
18	2, 11, 17	sylanc 473	. . 3 ⊢ (R ∈ U → if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V)
19	18	adantr 391	. 2 ⊢ ((R ∈ U ⋀ A ∈ W) → if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V)
20		eqid 1478	. . 3 ⊢ if(Z ≠ ∅, ∪Z, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X)
21		unieq 2514	. . . . . . . . . 10 ⊢ (u = Z → ∪u = ∪Z)
22	21	ifeq1d 2373	. . . . . . . . 9 ⊢ (u = Z → if(u ≠ ∅, ∪u, ℘∪X) = if(u ≠ ∅, ∪Z, ℘∪X))
23		neeq1 1593	. . . . . . . . . 10 ⊢ (u = Z → (u ≠ ∅ ↔ Z ≠ ∅))
24	23	ifbid 2376	. . . . . . . . 9 ⊢ (u = Z → if(u ≠ ∅, ∪Z, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X))
25	22, 24	eqtrd 1510	. . . . . . . 8 ⊢ (u = Z → if(u ≠ ∅, ∪u, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X))
26	25	eqeq2d 1489	. . . . . . 7 ⊢ (u = Z → ( if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪X) ↔ if(Z ≠ ∅, ∪Z, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X)))
27	26	ceqsexgv 1891	. . . . . 6 ⊢ (Z ∈ V → (∃u(u = Z ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪X)) ↔ if(Z ≠ ∅, ∪Z, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X)))
28	15, 27	syl 10	. . . . 5 ⊢ (R ∈ U → (∃u(u = Z ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪X)) ↔ if(Z ≠ ∅, ∪Z, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X)))
29	28	3ad2ant1 802	. . . 4 ⊢ ((R ∈ U ⋀ A ∈ W ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V) → (∃u(u = Z ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪X)) ↔ if(Z ≠ ∅, ∪Z, ℘∪X) = if(Z ≠ ∅, ∪Z, ℘∪X)))
30		unieq 2514	. . . . . . . . . . . . 13 ⊢ (r = R → ∪r = ∪R)
31	30	unieqd 2516	. . . . . . . . . . . 12 ⊢ (r = R → ∪∪r = ∪∪R)
32		rabeq 1812	. . . . . . . . . . . 12 ⊢ (∪∪r = ∪∪R → {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} = {x ∈ ∪∪R∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))})
33	31, 32	syl 10	. . . . . . . . . . 11 ⊢ (r = R → {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} = {x ∈ ∪∪R∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))})
34		breq 2626	. . . . . . . . . . . . . 14 ⊢ (r = R → (yrx ↔ yRx))
35	34	ralbidv 1666	. . . . . . . . . . . . 13 ⊢ (r = R → (∀y ∈ w yrx ↔ ∀y ∈ w yRx))
36		breq 2626	. . . . . . . . . . . . . . . 16 ⊢ (r = R → (zry ↔ zRy))
37	36	ralbidv 1666	. . . . . . . . . . . . . . 15 ⊢ (r = R → (∀z ∈ w zry ↔ ∀z ∈ w zRy))
38		breq 2626	. . . . . . . . . . . . . . 15 ⊢ (r = R → (xry ↔ xRy))
39	37, 38	imbi12d 628	. . . . . . . . . . . . . 14 ⊢ (r = R → ((∀z ∈ w zry → xry) ↔ (∀z ∈ w zRy → xRy)))
40	31, 39	raleq12d 1797	. . . . . . . . . . . . 13 ⊢ (r = R → (∀y ∈ ∪∪r(∀z ∈ w zry → xry) ↔ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy)))
41	35, 40	anbi12d 630	. . . . . . . . . . . 12 ⊢ (r = R → ((∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry)) ↔ (∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))))
42	41	rabbisdv 1810	. . . . . . . . . . 11 ⊢ (r = R → {x ∈ ∪∪R∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))})
43	33, 42	eqtrd 1510	. . . . . . . . . 10 ⊢ (r = R → {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))})
44	43	eqeq2d 1489	. . . . . . . . 9 ⊢ (r = R → (u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ↔ u = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))}))
45	31	unieqd 2516	. . . . . . . . . . . 12 ⊢ (r = R → ∪∪∪r = ∪∪∪R)
46		pweq 2407	. . . . . . . . . . . 12 ⊢ (∪∪∪r = ∪∪∪R → ℘∪∪∪r = ℘∪∪∪R)
47	45, 46	syl 10	. . . . . . . . . . 11 ⊢ (r = R → ℘∪∪∪r = ℘∪∪∪R)
48	47	ifeq2d 2374	. . . . . . . . . 10 ⊢ (r = R → if(u ≠ ∅, ∪u, ℘∪∪∪r) = if(u ≠ ∅, ∪u, ℘∪∪∪R))
49	48	eqeq2d 1489	. . . . . . . . 9 ⊢ (r = R → (v = if(u ≠ ∅, ∪u, ℘∪∪∪r) ↔ v = if(u ≠ ∅, ∪u, ℘∪∪∪R)))
50	44, 49	anbi12d 630	. . . . . . . 8 ⊢ (r = R → ((u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)) ↔ (u = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R))))
51	50	exbidv 1281	. . . . . . 7 ⊢ (r = R → (∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)) ↔ ∃u(u = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R))))
52		raleq1 1789	. . . . . . . . . . . 12 ⊢ (w = A → (∀y ∈ w yRx ↔ ∀y ∈ A yRx))
53		raleq1 1789	. . . . . . . . . . . . . 14 ⊢ (w = A → (∀z ∈ w zRy ↔ ∀z ∈ A zRy))
54	53	imbi1d 615	. . . . . . . . . . . . 13 ⊢ (w = A → ((∀z ∈ w zRy → xRy) ↔ (∀z ∈ A zRy → xRy)))
55	54	ralbidv 1666	. . . . . . . . . . . 12 ⊢ (w = A → (∀y ∈ ∪∪R(∀z ∈ w zRy → xRy) ↔ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy)))
56	52, 55	anbi12d 630	. . . . . . . . . . 11 ⊢ (w = A → ((∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy)) ↔ (∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))))
57	56	rabbisdv 1810	. . . . . . . . . 10 ⊢ (w = A → {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))} = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))})
58	57	eqeq2d 1489	. . . . . . . . 9 ⊢ (w = A → (u = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))} ↔ u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))}))
59	58	anbi1d 619	. . . . . . . 8 ⊢ (w = A → ((u = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R)) ↔ (u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R))))
60	59	exbidv 1281	. . . . . . 7 ⊢ (w = A → (∃u(u = {x ∈ ∪∪R∣(∀y ∈ w yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ w zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R)) ↔ ∃u(u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R))))
61		eqeq1 1484	. . . . . . . . 9 ⊢ (v = if(Z ≠ ∅, ∪Z, ℘∪X) → (v = if(u ≠ ∅, ∪u, ℘∪∪∪R) ↔ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪∪∪R)))
62	61	anbi2d 618	. . . . . . . 8 ⊢ (v = if(Z ≠ ∅, ∪Z, ℘∪X) → ((u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R)) ↔ (u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪∪∪R))))
63	62	exbidv 1281	. . . . . . 7 ⊢ (v = if(Z ≠ ∅, ∪Z, ℘∪X) → (∃u(u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪R)) ↔ ∃u(u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪∪∪R))))
64		moeq 1923	. . . . . . . . 9 ⊢ ∃*u u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))}
65		moeq 1923	. . . . . . . . . 10 ⊢ ∃*v v = if(u ≠ ∅, ∪u, ℘∪∪∪r)
66	65	ax-gen 965	. . . . . . . . 9 ⊢ ∀u∃*v v = if(u ≠ ∅, ∪u, ℘∪∪∪r)
67		moexexv 1442	. . . . . . . . 9 ⊢ ((∃*u u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ ∀u∃*v v = if(u ≠ ∅, ∪u, ℘∪∪∪r)) → ∃*v∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)))
68	64, 66, 67	mp2an 699	. . . . . . . 8 ⊢ ∃*v∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r))
69	68	a1i 8	. . . . . . 7 ⊢ ((r ∈ V ⋀ w ∈ V) → ∃*v∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)))
70		df-spw 8636	. . . . . . . 8 ⊢ supw = {⟨⟨r, w⟩, v⟩∣∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r))}
71		visset 1816	. . . . . . . . . . 11 ⊢ r ∈ V
72		visset 1816	. . . . . . . . . . 11 ⊢ w ∈ V
73	71, 72	pm3.2i 285	. . . . . . . . . 10 ⊢ (r ∈ V ⋀ w ∈ V)
74	73	biantrur 727	. . . . . . . . 9 ⊢ (∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)) ↔ ((r ∈ V ⋀ w ∈ V) ⋀ ∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r))))
75	74	oprabbii 4003	. . . . . . . 8 ⊢ {⟨⟨r, w⟩, v⟩∣∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r))} = {⟨⟨r, w⟩, v⟩∣((r ∈ V ⋀ w ∈ V) ⋀ ∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)))}
76	70, 75	eqtr 1498	. . . . . . 7 ⊢ supw = {⟨⟨r, w⟩, v⟩∣((r ∈ V ⋀ w ∈ V) ⋀ ∃u(u = {x ∈ ∪∪r∣(∀y ∈ w yrx ⋀ ∀y ∈ ∪∪r(∀z ∈ w zry → xry))} ⋀ v = if(u ≠ ∅, ∪u, ℘∪∪∪r)))}
77	51, 60, 63, 69, 76	oprabvalig 4030	. . . . . 6 ⊢ ((R ∈ V ⋀ A ∈ V ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V) → (∃u(u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪∪∪R)) → (R supw A) = if(Z ≠ ∅, ∪Z, ℘∪X)))
78		elisset 1820	. . . . . 6 ⊢ (R ∈ U → R ∈ V)
79		elisset 1820	. . . . . 6 ⊢ (A ∈ W → A ∈ V)
80		id 59	. . . . . 6 ⊢ ( if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V → if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V)
81	77, 78, 79, 80	syl3an 870	. . . . 5 ⊢ ((R ∈ U ⋀ A ∈ W ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) ∈ V) → (∃u(u = {x ∈ ∪∪R∣(∀y ∈ A yRx ⋀ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))} ⋀ if(Z ≠ ∅, ∪Z, ℘∪X) = if(u ≠ ∅, ∪u, ℘∪∪∪R)) → (R supw A) = if(Z ≠ ∅, ∪Z, ℘∪X)))
82		raleq1 1789	. . . . . . . . . . . . 13 ⊢ (X = ∪∪R → (∀y ∈ X (∀z ∈ A zRy → xRy) ↔ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy)))
83	6, 82	ax-mp 7	. . . . . . . . . . . 12 ⊢ (∀y ∈ X (∀z ∈ A zRy → xRy) ↔ ∀y ∈ ∪∪R(∀z ∈ A zRy → xRy))
84	83	anbi2i 482	. . . . . . . . . . 11 ⊢ ((∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zR