Metamath Proof Explorer

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 eqtrid 
 |-  ( -. 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