Theorem spwval2 8636

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

Hypotheses

Ref	Expression
spwval2.1	|- X = U.U.R
spwval2.2	|- Z = {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}

Assertion

Ref	Expression
spwval2	|- ((R e. U /\ A e. W) -> (R supw A) = if(Z =/= (/), U.Z, P~U.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 2378	. . . . 5 |- ((U.Z e. V /\ P~U.X e. V) -> if(Z =/= (/), U.Z, P~U.X) e. V)
2	1	ancoms 436	. . . 4 |- ((P~U.X e. V /\ U.Z e. V) -> if(Z =/= (/), U.Z, P~U.X) e. V)
3		uniexg 2868	. . . . . . . 8 |- (R e. U -> U.R e. V)
4		uniexg 2868	. . . . . . . 8 |- (U.R e. V -> U.U.R e. V)
5	3, 4	syl 10	. . . . . . 7 |- (R e. U -> U.U.R e. V)
6		spwval2.1	. . . . . . 7 |- X = U.U.R
7	5, 6	syl5eqel 1551	. . . . . 6 |- (R e. U -> X e. V)
8		uniexg 2868	. . . . . 6 |- (X e. V -> U.X e. V)
9	7, 8	syl 10	. . . . 5 |- (R e. U -> U.X e. V)
10		pwexg 2743	. . . . 5 |- (U.X e. V -> P~U.X e. V)
11	9, 10	syl 10	. . . 4 |- (R e. U -> P~U.X e. V)
12		rabexg 2721	. . . . . . 7 |- (X e. V -> {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. V)
13	7, 12	syl 10	. . . . . 6 |- (R e. U -> {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. V)
14		spwval2.2	. . . . . 6 |- Z = {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}
15	13, 14	syl5eqel 1551	. . . . 5 |- (R e. U -> Z e. V)
16		uniexg 2868	. . . . 5 |- (Z e. V -> U.Z e. V)
17	15, 16	syl 10	. . . 4 |- (R e. U -> U.Z e. V)
18	2, 11, 17	sylanc 471	. . 3 |- (R e. U -> if(Z =/= (/), U.Z, P~U.X) e. V)
19	18	adantr 389	. 2 |- ((R e. U /\ A e. W) -> if(Z =/= (/), U.Z, P~U.X) e. V)
20		eqid 1475	. . 3 |- if(Z =/= (/), U.Z, P~U.X) = if(Z =/= (/), U.Z, P~U.X)
21		unieq 2507	. . . . . . . . . 10 |- (u = Z -> U.u = U.Z)
22	21	ifeq1d 2367	. . . . . . . . 9 |- (u = Z -> if(u =/= (/), U.u, P~U.X) = if(u =/= (/), U.Z, P~U.X))
23		neeq1 1589	. . . . . . . . . 10 |- (u = Z -> (u =/= (/) <-> Z =/= (/)))
24	23	ifbid 2370	. . . . . . . . 9 |- (u = Z -> if(u =/= (/), U.Z, P~U.X) = if(Z =/= (/), U.Z, P~U.X))
25	22, 24	eqtrd 1506	. . . . . . . 8 |- (u = Z -> if(u =/= (/), U.u, P~U.X) = if(Z =/= (/), U.Z, P~U.X))
26	25	eqeq2d 1485	. . . . . . 7 |- (u = Z -> (if(Z =/= (/), U.Z, P~U.X) = if(u =/= (/), U.u, P~U.X) <-> if(Z =/= (/), U.Z, P~U.X) = if(Z =/= (/), U.Z, P~U.X)))
27	26	ceqsexgv 1886	. . . . . 6 |- (Z e. V -> (E.u(u = Z /\ if(Z =/= (/), U.Z, P~U.X) = if(u =/= (/), U.u, P~U.X)) <-> if(Z =/= (/), U.Z, P~U.X) = if(Z =/= (/), U.Z, P~U.X)))
28	15, 27	syl 10	. . . . 5 |- (R e. U -> (E.u(u = Z /\ if(Z =/= (/), U.Z, P~U.X) = if(u =/= (/), U.u, P~U.X)) <-> if(Z =/= (/), U.Z, P~U.X) = if(Z =/= (/), U.Z, P~U.X)))
29	28	3ad2ant1 799	. . . 4 |- ((R e. U /\ A e. W /\ if(Z =/= (/), U.Z, P~U.X) e. V) -> (E.u(u = Z /\ if(Z =/= (/), U.Z, P~U.X) = if(u =/= (/), U.u, P~U.X)) <-> if(Z =/= (/), U.Z, P~U.X) = if(Z =/= (/), U.Z, P~U.X)))
30		unieq 2507	. . . . . . . . . . . . 13 |- (r = R -> U.r = U.R)
31	30	unieqd 2509	. . . . . . . . . . . 12 |- (r = R -> U.U.r = U.U.R)
32		rabeq 1807	. . . . . . . . . . . 12 |- (U.U.r = U.U.R -> {x e. U.U.r | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} = {x e. U.U.R | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))})
33	31, 32	syl 10	. . . . . . . . . . 11 |- (r = R -> {x e. U.U.r | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} = {x e. U.U.R | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))})
34		breq 2618	. . . . . . . . . . . . . 14 |- (r = R -> (yrx <-> yRx))
35	34	ralbidv 1662	. . . . . . . . . . . . 13 |- (r = R -> (A.y e. w yrx <-> A.y e. w yRx))
36		breq 2618	. . . . . . . . . . . . . . . 16 |- (r = R -> (zry <-> zRy))
37	36	ralbidv 1662	. . . . . . . . . . . . . . 15 |- (r = R -> (A.z e. w zry <-> A.z e. w zRy))
38		breq 2618	. . . . . . . . . . . . . . 15 |- (r = R -> (xry <-> xRy))
39	37, 38	imbi12d 625	. . . . . . . . . . . . . 14 |- (r = R -> ((A.z e. w zry -> xry) <-> (A.z e. w zRy -> xRy)))
40	31, 39	raleq12d 1793	. . . . . . . . . . . . 13 |- (r = R -> (A.y e. U.U.r(A.z e. w zry -> xry) <-> A.y e. U.U.R(A.z e. w zRy -> xRy)))
41	35, 40	anbi12d 627	. . . . . . . . . . . 12 |- (r = R -> ((A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry)) <-> (A.y e. w yRx /\ A.y e. U.U.R(A.z e. w zRy -> xRy))))
42	41	rabbisdv 1805	. . . . . . . . . . 11 |- (r = R -> {x e. U.U.R | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} = {x e. U.U.R | (A.y e. w yRx /\ A.y e. U.U.R(A.z e. w zRy -> xRy))})
43	33, 42	eqtrd 1506	. . . . . . . . . 10 |- (r = R -> {x e. U.U.r | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} = {x e. U.U.R | (A.y e. w yRx /\ A.y e. U.U.R(A.z e. w zRy -> xRy))})
44	43	eqeq2d 1485	. . . . . . . . 9 |- (r = R -> (u = {x e. U.U.r | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} <-> u = {x e. U.U.R | (A.y e. w yRx /\ A.y e. U.U.R(A.z e. w zRy -> xRy))}))
45	31	unieqd 2509	. . . . . . . . . . . 12 |- (r = R -> U.U.U.r = U.U.U.R)
46		pweq 2401	. . . . . . . . . . . 12 |- (U.U.U.r = U.U.U.R -> P~U.U.U.r = P~U.U.U.R)
47	45, 46	syl 10	. . . . . . . . . . 11 |- (r = R -> P~U.U.U.r = P~U.U.U.R)
48	47	ifeq2d 2368	. . . . . . . . . 10 |- (r = R -> if(u =/= (/), U.u, P~U.U.U.r) = if(u =/= (/), U.u, P~U.U.U.R))
49	48	eqeq2d 1485	. . . . . . . . 9 |- (r = R -> (v = if(u =/= (/), U.u, P~U.U.U.r) <-> v = if(u =/= (/), U.u, P~U.U.U.R)))
50	44, 49	anbi12d 627	. . . . . . . 8 |- (r = R -> ((u = {x e. U.U.r | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} /\ v = if(u =/= (/), U.u, P~U.U.U.r)) <-> (u = {x e. U.U.R | (A.y e. w yRx /\ A.y e. U.U.R(A.z e. w zRy -> xRy))} /\ v = if(u =/= (/), U.u, P~U.U.U.R))))
51	50	exbidv 1279	. . . . . . 7 |- (r = R -> (E.u(u = {x e. U.U.r | (A.y e. w yrx /\ A.y e. U.U.r(A.z e. w zry -> xry))} /\ v = if(u =/= (/), U.u, P~U.U.U.r)) <-> E.u(u = {x e. U.U.R | (A.y e. w yRx /\ A.y e. U.U.R(A.z e. w zRy -> xRy))} /\ v = if(u =/= (/), U.u, P~U.U.U.R))))
52		raleq1 1785	. . . . . . . . . . . 12