Theorem inposet 14620

Description: Inclusion partially orders any set.

Hypothesis

Ref	Expression
inposet.1	|- C = {<.x, y>. | x C_ 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 4088	. . . 4 |- Rel (A X. A)
2		relin2 4099	. . . 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 3341	. . . . . . . . . . . . . . 15 |- (a = x -> (aCz <-> xCz))
5		sseq1 2637	. . . . . . . . . . . . . . 15 |- (a = x -> (a C_ y <-> x C_ y))
6	4, 5	imbi12d 688	. . . . . . . . . . . . . 14 |- (a = x -> ((aCz -> a C_ y) <-> (xCz -> x C_ y)))
7	6	imbi2d 674	. . . . . . . . . . . . 13 |- (a = x -> ((zCy -> (aCz -> a C_ y)) <-> (zCy -> (xCz -> x C_ y))))
8		breq2 3342	. . . . . . . . . . . . . . 15 |- (b = y -> (zCb <-> zCy))
9		sseq2 2639	. . . . . . . . . . . . . . . 16 |- (b = y -> (a C_ b <-> a C_ y))
10	9	imbi2d 674	. . . . . . . . . . . . . . 15 |- (b = y -> ((aCz -> a C_ b) <-> (aCz -> a C_ y)))
11	8, 10	imbi12d 688	. . . . . . . . . . . . . 14 |- (b = y -> ((zCb -> (aCz -> a C_ b)) <-> (zCy -> (aCz -> a C_ y))))
12		visset 2295	. . . . . . . . . . . . . . . 16 |- z e. _V
13		visset 2295	. . . . . . . . . . . . . . . 16 |- b e. _V
14		inposet.1	. . . . . . . . . . . . . . . 16 |- C = {<.x, y>. | x C_ y}
15	12, 13, 14	inposetlem 14618	. . . . . . . . . . . . . . 15 |- (zCb <-> z C_ b)
16		visset 2295	. . . . . . . . . . . . . . . . . 18 |- a e. _V
17	16, 12, 14	inposetlem 14618	. . . . . . . . . . . . . . . . 17 |- (aCz <-> a C_ z)
18		sstr2 2623	. . . . . . . . . . . . . . . . 17 |- (a C_ z -> (z C_ b -> a C_ b))
19	17, 18	sylbi 216	. . . . . . . . . . . . . . . 16 |- (aCz -> (z C_ b -> a C_ b))
20	19	com12 14	. . . . . . . . . . . . . . 15 |- (z C_ b -> (aCz -> a C_ b))
21	15, 20	sylbi 216	. . . . . . . . . . . . . 14 |- (zCb -> (aCz -> a C_ b))
22	11, 21	chvarv 1712	. . . . . . . . . . . . 13 |- (zCy -> (aCz -> a C_ y))
23	7, 22	chvarv 1712	. . . . . . . . . . . 12 |- (zCy -> (xCz -> x C_ y))
24	23	3ad2ant3 899	. . . . . . . . . . 11 |- ((z e. A /\ y e. A /\ zCy) -> (xCz -> x C_ y))
25	24	com12 14	. . . . . . . . . 10 |- (xCz -> ((z e. A /\ y e. A /\ zCy) -> x C_ y))
26	25	3ad2ant3 899	. . . . . . . . 9 |- ((x e. A /\ z e. A /\ xCz) -> ((z e. A /\ y e. A /\ zCy) -> x C_ y))
27	26	imp 377	. . . . . . . 8 |- (((x e. A /\ z e. A /\ xCz) /\ (z e. A /\ y e. A /\ zCy)) -> x C_ y)
28		simp1 876	. . . . . . . . 9 |- ((x e. A /\ z e. A /\ xCz) -> x e. A)
29		simp2 877	. . . . . . . . 9 |- ((z e. A /\ y e. A /\ zCy) -> y e. A)
30	28, 29	anim12i 360	. . . . . . . 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 310	. . . . . . 7 |- (((x e. A /\ z e. A /\ xCz) /\ (z e. A /\ y e. A /\ zCy)) -> (x C_ y /\ (x e. A /\ y e. A)))
32		brinxp2 4057	. . . . . . . 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 2295	. . . . . . . 8 |- y e. _V
35		brinxp2 4057	. . . . . . . 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 504	. . . . . 6 |- ((x(C i^i (A X. A))z /\ z(C i^i (A X. A))y) -> (x C_ y /\ (x e. A /\ y e. A)))
38	37	19.23aiv 1674	. . . . 5 |- (E.z(x(C i^i (A X. A))z /\ z(C i^i (A X. A))y) -> (x C_ y /\ (x e. A /\ y e. A)))
39	38	ssopab2i 3574	. . . 4 |- {<.x, y>. | E.z(x(C i^i (A X. A))z /\ z(C i^i (A X. A))y)} C_ {<.x, y>. | (x C_ y /\ (x e. A /\ y e. A))}
40		df-co 4003	. . . 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 2792	. . . . 5 |- (C i^i (A X. A)) = ({<.x, y>. | x C_ y} i^i (A X. A))
42		df-xp 4000	. . . . . 6 |- (A X. A) = {<.x, y>. | (x e. A /\ y e. A)}
43	42	ineq2i 2793	. . . . 5 |- ({<.x, y>. | x C_ y} i^i (A X. A)) = ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)})
44		inopab 4108	. . . . 5 |- ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)}) = {<.x, y>. | (x C_ y /\ (x e. A /\ y e. A))}
45	41, 43, 44	3eqtri 1912	. . . 4 |- (C i^i (A X. A)) = {<.x, y>. | (x C_ y /\ (x e. A /\ y e. A))}
46	39, 40, 45	3sstr4i 2656	. . 3 |- ((C i^i (A X. A)) o. (C i^i (A X. A))) C_ (C i^i (A X. A))
47		asymref 4308	. . . 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 3197	. . . . . . . 8 |- U.(C i^i (A X. A)) C_ (U.C i^i U.(A X. A))
49		uniss 3199	. . . . . . . 8 |- (U.(C i^i (A X. A)) C_ (U.C i^i U.(A X. A)) -> U.U.(C i^i (A X. A)) C_ U.(U.C i^i U.(A X. A)))
50	48, 49	ax-mp 7	. . . . . . 7 |- U.U.(C i^i (A X. A)) C_ U.(U.C i^i U.(A X. A))
51	50	sseli 2617	. . . . . 6 |- (a e. U.U.(C i^i (A X. A)) -> a e. U.(U.C i^i U.(A X. A)))
52		uniin 3197	. . . . . . 7 |- U.(U.C i^i U.(A X. A)) C_ (U.U.C i^i U.U.(A X. A))
53	52	sseli 2617	. . . . . 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 2786	. . . . . . 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 4094	. . . . . . . . . 10 |- U.U.(A X. A) C_ (A u. A)
56	55	sseli 2617	. . . . . . . . 9 |- (a e. U.U.(A X. A) -> a e. (A u. A))
57		unidm 2743	. . . . . . . . 9 |- (A u. A) = A
58	56, 57	syl6eleq 1981	. . . . . . . 8 |- (a e. U.U.(A X. A) -> a e. A)
59	58	adantl 424	. . . . . . 7 |- ((a e. U.U.C /\ a e. U.U.(A X. A)) -> a e. A)
60	54, 59	sylbi 216	. . . . . 6 |- (a e. (U.U.C i^i U.U.(A X. A)) -> a e. A)
61	51, 53, 60	3syl 24	. . . . 5 |- (a e. U.U.(C i^i (A X. A)) -> a e. A)
62	16, 13, 14	inposetlem 14618	. . . . . . . . . . . 12 |- (aCb <-> a C_ b)
63	13, 16, 14	inposetlem 14618	. . . . . . . . . . . . . . 15 |- (bCa <-> b C_ a)
64		eqss 2631	. . . . . . . . . . . . . . . . 17 |- (a = b <-> (a C_ b /\ b C_ a))
65	64	biimpri 169	. . . . . . . . . . . . . . . 16 |- ((a C_ b /\ b C_ a) -> a = b)
66	65	expcom 403	. . . . . . . . . . . . . . 15 |- (b C_ a -> (a C_ b -> a = b))
67	63, 66	sylbi 216	. . . . . . . . . . . . . 14 |- (bCa -> (a C_ b -> a = b))
68	67	3ad2ant3 899	. . . . . . . . . . . . 13 |- ((b e. A /\ a e. A /\ bCa) -> (a C_ b -> a = b))
69	68	com12 14	. . . . . . . . . . . 12 |- (a C_ b -> ((b e. A /\ a e. A /\ bCa) -> a = b))
70	62, 69	sylbi 216	. . . . . . . . . . 11 |- (aCb -> ((b e. A /\ a e. A /\ bCa) -> a = b))
71	70	3ad2ant3 899	. . . . . . . . . 10 |- ((a e. A /\ b e. A /\ aCb) -> ((b e. A /\ a e. A /\ bCa) -> a = b))
72	71	imp 377	. . . . . . . . 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) /\ (b e. A /\ a e. A /\ bCa)) -> a = b))
74		brinxp2 4057	. . . . . . . . . 10 |- (b e. _V -> (a(C i^i (A X. A))b <-> (a e. A /\ b e. A /\ aCb)))
75	13, 74	ax-mp 7	. . . . . . . . 9 |- (a(C i^i (A X. A))b <-> (a e. A /\ b e. A /\ aCb))
76		brinxp2 4057	. . . . . . . . . 10 |- (a e. _V -> (b(C i^i (A X. A))a <-> (b e. A /\ a e. A /\ bCa)))
77	16, 76	ax-mp 7	. . . . . . . . 9 |- (b(C i^i (A X. A))a <-> (b e. A /\ a e. A /\ bCa))
78	75, 77	anbi12i 540	. . . . . . . 8 |- ((a(C i^i (A X. A))b /\ b(C i^i (A X. A))a) <-> ((a e. A /\ b e. A /\ aCb) /\ (b e. A /\ a e. A /\ bCa)))
79	73, 78	syl5ib 223	. . . . . . 7 |- (a e. A -> ((a(C i^i (A X. A))b /\ b(C i^i (A X. A))a) -> a = b))
80		id 73	. . . . . . . . . . . 12 |- (b e. A -> b e. A)
81		ssid 2634	. . . . . . . . . . . . . 14 |- b C_ b
82	13, 13, 14	inposetlem 14618	. . . . . . . . . . . . . 14 |- (bCb <-> b C_ b)
83	81, 82	mpbir 207	. . . . . . . . . . . . 13 |- bCb
84	83	a1i 8	. . . . . . . . . . . 12 |- (b e. A -> bCb)
85	80, 80, 84	3jca 1050	. . . . . . . . . . 11 |- (b e. A -> (b e. A /\ b e. A /\ bCb))
86		brinxp2 4057	. . . . . . . . . . 11 |- (b e. A -> (b(C i^i (A X. A))b <-> (b e. A /\ b e. A /\ bCb)))
87	85, 86	mpbird 213	. . . . . . . . . 10 |- (b e. A -> b(C i^i (A X. A))b)
88		anidmdbi 481	. . . . . . . . . 10 |- ((b e. A -> (b(C i^i (A X. A))b /\ b(C i^i (A X. A))b)) <-> (b e. A -> b(C i^i (A X. A))b))
89	87, 88	mpbir 207	. . . . . . . . 9 |- (b e. A -> (b(C i^i (A X. A))b /\ b(C i^i (A X. A))b))
90		eleq1 1957	. . . . . . . . . 10 |- (a = b -> (a e. A <-> b e. A))
91		breq1 3341	. . . . . . . . . . 11 |- (a = b -> (a(C i^i (A X. A))b <-> b(C i^i (A X. A))b))
92		breq2 3342	. . . . . . . . . . 11 |- (a = b -> (b(C i^i (A X. A))a <-> b(C i^i (A X. A))b))
93	91, 92	anbi12d 690	. . . . . . . . . 10 |- (a = b -> ((a(C i^i (A X. A))b /\ b(C i^i (A X. A))a) <-> (b(C i^i (A X. A))b /\ b(C i^i (A X. A))b)))
94	90, 93	imbi12d 688	. . . . . . . . 9 |- (a = b -> ((a e. A -> (a(C i^i (A X. A))b /\ b(C i^i (A X. A))a)) <-> (b e. A -> (b(C i^i (A X. A))b /\ b(C i^i (A X. A))b))))
95	89, 94	mpbiri 211	. . . . . . . 8 |- (a = b -> (a e. A -> (a(C i^i (A X. A))b /\ b(C i^i (A X. A))a)))
96	95	com12 14	. . . . . . 7 |- (a e. A -> (a = b -> (a(C i^i (A X. A))b /\ b(C i^i (A X. A))a)))
97	79, 96	impbid 574	. . . . . 6 |- (a e. A -> ((a(C i^i (A X. A))b /\ b(C i^i (A X. A))a) <-> a = b))
98	97	19.21aiv 1664	. . . . 5 |- (a e. A -> A.b((a(C i^i (A X. A))b /\ b(C i^i (A X. A))a) <-> a = b))
99	61, 98	syl 12	. . . 4 |- (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))
100	47, 99	mprgbir 2163	. . 3 |- ((C i^i (A X. A)) i^i `'(C i^i (A X. A))) = ( _I |` U.U.(C i^i (A X. A)))
101	3, 46, 100	3pm3.2i 1048	. 2 |- (Rel (C i^i (A X. A)) /\ ((C i^i (A X. A)) o. (C i^i (A X. A))) C_ (C i^i (A X. A)) /\ ((C i^i (A X. A)) i^i `'(C i^i (A X. A))) = ( _I |` U.U.(C i^i (A X. A))))
102		xpexg 4095	. . . . 5 |- ((A e. B /\ A e. B) -> (A X. A) e. _V)
103	102	anidms 480	. . . 4 |- (A e. B -> (A X. A) e. _V)
104		inex1g 3454	. . . . 5 |- ((A X. A) e. _V -> ((A X. A) i^i C) e. _V)
105		incom 2787	. . . . 5 |- (C i^i (A X. A)) = ((A X. A) i^i C)
106	104, 105	syl5eqel 1975	. . . 4 |- ((A X. A) e. _V -> (C i^i (A X. A)) e. _V)
107	103, 106	syl 12	. . 3 |- (A e. B -> (C i^i (A X. A)) e. _V)
108		isps 9988	. . 3 |- ((C i^i (A X. A)) e. _V -> ((C i^i (A X. A)) e. Poset <-> (Rel (C i^i (A X. A)) /\ ((C i^i (A X. A)) o. (C i^i (A X. A))) C_ (C i^i (A X. A)) /\ ((C i^i (A X. A)) i^i `'(C i^i (A X. A))) = ( _I |` U.U.(C i^i (A X. A))))))
109	107, 108	syl 12	. 2 |- (A e. B -> ((C i^i (A X. A)) e. Poset <-> (Rel (C i^i (A X. A)) /\ ((C i^i (A X. A)) o. (C i^i (A X. A))) C_ (C i^i (A X. A)) /\ ((C i^i (A X. A)) i^i `'(C i^i (A X. A))) = ( _I |` U.U.(C i^i (A X. A))))))
110	101, 109	mpbiri 211	1 |- (A e. B -> (C i^i (A X. A)) e. Poset)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  U.cuni 3177   class class class wbr 3338  {copab 3395   _I cid 3582   X. cxp 3984  `'ccnv 3985   |` cres 3988   o. ccom 3990  Rel wrel 3991  Posetcps 9980

This theorem is referenced by:  toplat 14638

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-res 4006  df-ps 9984

Copyright terms: Public domain