Theorem inposet 10578

Description: Inclusion partially orders any set.

Hypothesis

Ref	Expression
inposet.1	|- C = {<.x, y>. | x (_ y}

Assertion

Ref	Expression
inposet	|- (A e. B -> (C i^i (A X. A)) e. Poset)

Distinct variable groups:   x,A,y   x,C,y

Proof of Theorem inposet

Step	Hyp	Ref	Expression
1		relxp 3312	. . . 4 |- Rel (A X. A)
2		relin2 3320	. . . 4 |- (Rel (A X. A) -> Rel (C i^i (A X. A)))
3	1, 2	ax-mp 7	. . 3 |- Rel (C i^i (A X. A))
4		breq1 2677	. . . . . . . . . . . . . . 15 |- (a = x -> (aCz <-> xCz))
5		sseq1 2133	. . . . . . . . . . . . . . 15 |- (a = x -> (a (_ y <-> x (_ y))
6	4, 5	imbi12d 637	. . . . . . . . . . . . . 14 |- (a = x -> ((aCz -> a (_ y) <-> (xCz -> x (_ y)))
7	6	imbi2d 623	. . . . . . . . . . . . 13 |- (a = x -> ((zCy -> (aCz -> a (_ y)) <-> (zCy -> (xCz -> x (_ y))))
8		breq2 2678	. . . . . . . . . . . . . . 15 |- (b = y -> (zCb <-> zCy))
9		sseq2 2134	. . . . . . . . . . . . . . . 16 |- (b = y -> (a (_ b <-> a (_ y))
10	9	imbi2d 623	. . . . . . . . . . . . . . 15 |- (b = y -> ((aCz -> a (_ b) <-> (aCz -> a (_ y)))
11	8, 10	imbi12d 637	. . . . . . . . . . . . . 14 |- (b = y -> ((zCb -> (aCz -> a (_ b)) <-> (zCy -> (aCz -> a (_ y))))
12		visset 1860	. . . . . . . . . . . . . . . 16 |- z e. V
13		visset 1860	. . . . . . . . . . . . . . . 16 |- b e. V
14		inposet.1	. . . . . . . . . . . . . . . 16 |- C = {<.x, y>. | x (_ y}
15	12, 13, 14	inposetlem 10576	. . . . . . . . . . . . . . 15 |- (zCb <-> z (_ b)
16		visset 1860	. . . . . . . . . . . . . . . . . 18 |- a e. V
17	16, 12, 14	inposetlem 10576	. . . . . . . . . . . . . . . . 17 |- (aCz <-> a (_ z)
18		sstr2 2122	. . . . . . . . . . . . . . . . 17 |- (a (_ z -> (z (_ b -> a (_ b))
19	17, 18	sylbi 206	. . . . . . . . . . . . . . . 16 |- (aCz -> (z (_ b -> a (_ b))
20	19	com12 11	. . . . . . . . . . . . . . 15 |- (z (_ b -> (aCz -> a (_ b))
21	15, 20	sylbi 206	. . . . . . . . . . . . . 14 |- (zCb -> (aCz -> a (_ b))
22	11, 21	chvarv 1369	. . . . . . . . . . . . 13 |- (zCy -> (aCz -> a (_ y))
23	7, 22	chvarv 1369	. . . . . . . . . . . 12 |- (zCy -> (xCz -> x (_ y))
24	23	3ad2ant3 814	. . . . . . . . . . 11 |- ((z e. A /\ y e. A /\ zCy) -> (xCz -> x (_ y))
25	24	com12 11	. . . . . . . . . 10 |- (xCz -> ((z e. A /\ y e. A /\ zCy) -> x (_ y))
26	25	3ad2ant3 814	. . . . . . . . 9 |- ((x e. A /\ z e. A /\ xCz) -> ((z e. A /\ y e. A /\ zCy) -> x (_ y))
27	26	imp 357	. . . . . . . 8 |- (((x e. A /\ z e. A /\ xCz) /\ (z e. A /\ y e. A /\ zCy)) -> x (_ y)
28		3simp1 800	. . . . . . . . 9 |- ((x e. A /\ z e. A /\ xCz) -> x e. A)
29		3simp2 801	. . . . . . . . 9 |- ((z e. A /\ y e. A /\ zCy) -> y e. A)
30	28, 29	anim12i 340	. . . . . . . 8 |- (((x e. A /\ z e. A /\ xCz) /\ (z e. A /\ y e. A /\ zCy)) -> (x e. A /\ y e. A))
31	27, 30	jca 295	. . . . . . 7 |- (((x e. A /\ z e. A /\ xCz) /\ (z e. A /\ y e. A /\ zCy)) -> (x (_ y /\ (x e. A /\ y e. A)))
32		brinxp2 3288	. . . . . . . 8 |- (z e. V -> (x(C i^i (A X. A))z <-> (x e. A /\ z e. A /\ xCz)))
33	12, 32	ax-mp 7	. . . . . . 7 |- (x(C i^i (A X. A))z <-> (x e. A /\ z e. A /\ xCz))
34		visset 1860	. . . . . . . 8 |- y e. V
35		brinxp2 3288	. . . . . . . 8 |- (y e. V -> (z(C i^i (A X. A))y <-> (z e. A /\ y e. A /\ zCy)))
36	34, 35	ax-mp 7	. . . . . . 7 |- (z(C i^i (A X. A))y <-> (z e. A /\ y e. A /\ zCy))
37	31, 33, 36	syl2anb 466	. . . . . 6 |- ((x(C i^i (A X. A))z /\ z(C i^i (A X. A))y) -> (x (_ y /\ (x e. A /\ y e. A)))
38	37	19.23aiv 1337	. . . . 5 |- (E.z(x(C i^i (A X. A))z /\ z(C i^i (A X. A))y) -> (x (_ y /\ (x e. A /\ y e. A)))
39	38	ssopab2i 2879	. . . 4 |- {<.x, y>. | E.z(x(C i^i (A X. A))z /\ z(C i^i (A X. A))y)} (_ {<.x, y>. | (x (_ y /\ (x e. A /\ y e. A))}
40		df-co 3244	. . . 4 |- ((C i^i (A X. A)) o. (C i^i (A X. A))) = {<.x, y>. | E.z(x(C i^i (A X. A))z /\ z(C i^i (A X. A))y)}
41	14	ineq1i 2264	. . . . 5 |- (C i^i (A X. A)) = ({<.x, y>. | x (_ y} i^i (A X. A))
42		df-xp 3241	. . . . . 6 |- (A X. A) = {<.x, y>. | (x e. A /\ y e. A)}
43	42	ineq2i 2265	. . . . 5 |- ({<.x, y>. | x (_ y} i^i (A X. A)) = ({<.x, y>. | x (_ y} i^i {<.x, y>. | (x e. A /\ y e. A)})
44		inopab 3325	. . . . 5 |- ({<.x, y>. | x (_ y} i^i {<.x, y>. | (x e. A /\ y e. A)}) = {<.x, y>. | (x (_ y /\ (x e. A /\ y e. A))}
45	41, 43, 44	3eqtri 1546	. . . 4 |- (C i^i (A X. A)) = {<.x, y>. | (x (_ y /\ (x e. A /\ y e. A))}
46	39, 40, 45	3sstr4i 2151	. . 3 |- ((C i^i (A X. A)) o. (C i^i (A X. A))) (_ (C i^i (A X. A))
47		asymref 3496	. . . 4 |- (((C i^i (A X. A)) i^i `'(C i^i (A X. A))) = (I |` U.U.(C i^i (A X. A))) <-> A.a e. U.U.(C i^i (A X. A))A.b((a(C i^i (A X. A))b /\ b(C i^i (A X. A))a) <-> a = b))
48		uniin 2574	. . . . . . . 8 |- U.(C i^i (A X. A)) (_ (U.C i^i U.(A X. A))
49		uniss 2575	. . . . . . . 8 |- (U.(C i^i (A X. A)) (_ (U.C i^i U.(A X. A)) -> U.U.(C i^i (A X. A)) (_ U.(U.C i^i U.(A X. A)))
50	48, 49	ax-mp 7	. . . . . . 7 |- U.U.(C i^i (A X. A)) (_ U.(U.C i^i U.(A X. A))
51	50	sseli 2116	. . . . . 6 |- (a e. U.U.(C i^i (A X. A)) -> a e. U.(U.C i^i U.(A X. A)))
52		uniin 2574	. . . . . . 7 |- U.(U.C i^i U.(A X. A)) (_ (U.U.C i^i U.U.(A X. A))
53	52	sseli 2116	. . . . . 6 |- (a e. U.(U.C i^i U.(A X. A)) -> a e. (U.U.C i^i U.U.(A X. A)))
54		elin 2258	. . . . . . 7 |- (a e. (U.U.C i^i U.U.(A X. A)) <-> (a e. U.U.C /\ a e. U.U.(A X. A)))
55		unixpss 3315	. . . . . . . . . 10 |- U.U.(A X. A) (_ (A u. A)
56	55	sseli 2116	. . . . . . . . 9 |- (a e. U.U.(A X. A) -> a e. (A u. A))
57		unidm 2226	. . . . . . . . 9 |- (A u. A) = A
58	56, 57	syl6eleq 1605	. . . . . . . 8 |- (a e. U.U.(A X. A) -> a e. A)
59	58	adantl 397	. . . . . . 7 |- ((a e. U.U.C /\ a e. U.U.(A X. A)) -> a e. A)
60	54, 59	sylbi 206	. . . . . 6 |- (a e. (U.U.C i^i U.U.(A X. A)) -> a e. A)
61	51, 53, 60	3syl 20	. . . . 5 |- (a e. U.U.(C i^i (A X. A)) -> a e. A)
62	16, 13, 14	inposetlem 10576	. . . . . . . . . . . 12 |- (aCb <-> a (_ b)
63	13, 16, 14	inposetlem 10576	. . . . . . . . . . . . . . 15 |- (bCa <-> b (_ a)
64		eqss 2128	. . . . . . . . . . . . . . . . 17 |- (a = b <-> (a (_ b /\ b (_ a))
65	64	biimpri 159	. . . . . . . . . . . . . . . 16 |- ((a (_ b /\ b (_ a) -> a = b)
66	65	expcom 381	. . . . . . . . . . . . . . 15 |- (b (_ a -> (a (_ b -> a = b))
67	63, 66	sylbi 206	. . . . . . . . . . . . . 14 |- (bCa -> (a (_ b -> a = b))
68	67	3ad2ant3 814	. . . . . . . . . . . . 13 |- ((b e. A /\ a e. A /\ bCa) -> (a (_ b -> a = b))
69	68	com12 11	. . . . . . . . . . . 12 |- (a (_ b -> ((b e. A /\ a e. A /\ bCa) -> a = b))
70	62, 69	sylbi 206	. . . . . . . . . . 11 |- (aCb -> ((b e. A /\ a e. A /\ bCa) -> a = b))
71	70	3ad2ant3 814	. . . . . . . . . 10 |- ((a e. A /\ b e. A /\ aCb) -> ((b e. A /\ a e. A /\ bCa) -> a = b))
72	71	imp 357	. . . . . . . . 9 |- (((a e. A /\ b e. A /\ aCb) /\ (b e. A /\ a e. A /\ bCa)) -> a = b)
73	72	a1i 8	. . . . . . . 8 |- (a e. A -> (((a e. A /\ b e. A /\ aCb