Theorem ipopos

Description: The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypothesis	ipopos.i	|- I = ( toInc ` F )
Assertion	ipopos	|- I e. Poset

Proof

Step	Hyp	Ref	Expression
1		ipopos.i	|- I = ( toInc ` F )
2	1	fvexi	|- I e. _V
3	2	a1i	|- ( F e. _V -> I e. _V )
4	1	ipobas	|- ( F e. _V -> F = ( Base ` I ) )
5		eqidd	|- ( F e. _V -> ( le ` I ) = ( le ` I ) )
6		ssid	|- a C_ a
7		eqid	|- ( le ` I ) = ( le ` I )
8	1 7	ipole	|- ( ( F e. _V /\ a e. F /\ a e. F ) -> ( a ( le ` I ) a <-> a C_ a ) )
9	8	3anidm23	|- ( ( F e. _V /\ a e. F ) -> ( a ( le ` I ) a <-> a C_ a ) )
10	6 9	mpbiri	|- ( ( F e. _V /\ a e. F ) -> a ( le ` I ) a )
11	1 7	ipole	|- ( ( F e. _V /\ a e. F /\ b e. F ) -> ( a ( le ` I ) b <-> a C_ b ) )
12	1 7	ipole	|- ( ( F e. _V /\ b e. F /\ a e. F ) -> ( b ( le ` I ) a <-> b C_ a ) )
13	12	3com23	|- ( ( F e. _V /\ a e. F /\ b e. F ) -> ( b ( le ` I ) a <-> b C_ a ) )
14	11 13	anbi12d	|- ( ( F e. _V /\ a e. F /\ b e. F ) -> ( ( a ( le ` I ) b /\ b ( le ` I ) a ) <-> ( a C_ b /\ b C_ a ) ) )
15		simpl	|- ( ( a C_ b /\ b C_ a ) -> a C_ b )
16		simpr	|- ( ( a C_ b /\ b C_ a ) -> b C_ a )
17	15 16	eqssd	|- ( ( a C_ b /\ b C_ a ) -> a = b )
18	14 17	syl6bi	|- ( ( F e. _V /\ a e. F /\ b e. F ) -> ( ( a ( le ` I ) b /\ b ( le ` I ) a ) -> a = b ) )
19		sstr	|- ( ( a C_ b /\ b C_ c ) -> a C_ c )
20	19	a1i	|- ( ( F e. _V /\ ( a e. F /\ b e. F /\ c e. F ) ) -> ( ( a C_ b /\ b C_ c ) -> a C_ c ) )
21	11	3adant3r3	|- ( ( F e. _V /\ ( a e. F /\ b e. F /\ c e. F ) ) -> ( a ( le ` I ) b <-> a C_ b ) )
22	1 7	ipole	|- ( ( F e. _V /\ b e. F /\ c e. F ) -> ( b ( le ` I ) c <-> b C_ c ) )
23	22	3adant3r1	|- ( ( F e. _V /\ ( a e. F /\ b e. F /\ c e. F ) ) -> ( b ( le ` I ) c <-> b C_ c ) )
24	21 23	anbi12d	|- ( ( F e. _V /\ ( a e. F /\ b e. F /\ c e. F ) ) -> ( ( a ( le ` I ) b /\ b ( le ` I ) c ) <-> ( a C_ b /\ b C_ c ) ) )
25	1 7	ipole	|- ( ( F e. _V /\ a e. F /\ c e. F ) -> ( a ( le ` I ) c <-> a C_ c ) )
26	25	3adant3r2	|- ( ( F e. _V /\ ( a e. F /\ b e. F /\ c e. F ) ) -> ( a ( le ` I ) c <-> a C_ c ) )
27	20 24 26	3imtr4d	|- ( ( F e. _V /\ ( a e. F /\ b e. F /\ c e. F ) ) -> ( ( a ( le ` I ) b /\ b ( le ` I ) c ) -> a ( le ` I ) c ) )
28	3 4 5 10 18 27	isposd	|- ( F e. _V -> I e. Poset )
29		fvprc	|- ( -. F e. _V -> ( toInc ` F ) = (/) )
30	1 29	syl5eq	|- ( -. F e. _V -> I = (/) )
31		0pos	|- (/) e. Poset
32	30 31	eqeltrdi	|- ( -. F e. _V -> I e. Poset )
33	28 32	pm2.61i	|- I e. Poset