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∈Poset

Proof

Step Hyp Ref Expression
1 ipopos.i ⊢I=toInc⁡F
2 1 fvexi ⊢I∈V
3 2 a1i ⊢F∈V→I∈V
4 1 ipobas ⊢F∈V→F=BaseI
5 eqidd ⊢F∈V→≤I=≤I
6 ssid ⊢a⊆a
7 eqid ⊢≤I=≤I
8 1 7 ipole ⊢F∈V∧a∈F∧a∈F→a≤Ia↔a⊆a
9 8 3anidm23 ⊢F∈V∧a∈F→a≤Ia↔a⊆a
10 6 9 mpbiri ⊢F∈V∧a∈F→a≤Ia
11 1 7 ipole ⊢F∈V∧a∈F∧b∈F→a≤Ib↔a⊆b
12 1 7 ipole ⊢F∈V∧b∈F∧a∈F→b≤Ia↔b⊆a
13 12 3com23 ⊢F∈V∧a∈F∧b∈F→b≤Ia↔b⊆a
14 11 13 anbi12d ⊢F∈V∧a∈F∧b∈F→a≤Ib∧b≤Ia↔a⊆b∧b⊆a
15 simpl ⊢a⊆b∧b⊆a→a⊆b
16 simpr ⊢a⊆b∧b⊆a→b⊆a
17 15 16 eqssd ⊢a⊆b∧b⊆a→a=b
18 14 17 syl6bi ⊢F∈V∧a∈F∧b∈F→a≤Ib∧b≤Ia→a=b
19 sstr ⊢a⊆b∧b⊆c→a⊆c
20 19 a1i ⊢F∈V∧a∈F∧b∈F∧c∈F→a⊆b∧b⊆c→a⊆c
21 11 3adant3r3 ⊢F∈V∧a∈F∧b∈F∧c∈F→a≤Ib↔a⊆b
22 1 7 ipole ⊢F∈V∧b∈F∧c∈F→b≤Ic↔b⊆c
23 22 3adant3r1 ⊢F∈V∧a∈F∧b∈F∧c∈F→b≤Ic↔b⊆c
24 21 23 anbi12d ⊢F∈V∧a∈F∧b∈F∧c∈F→a≤Ib∧b≤Ic↔a⊆b∧b⊆c
25 1 7 ipole ⊢F∈V∧a∈F∧c∈F→a≤Ic↔a⊆c
26 25 3adant3r2 ⊢F∈V∧a∈F∧b∈F∧c∈F→a≤Ic↔a⊆c
27 20 24 26 3imtr4d ⊢F∈V∧a∈F∧b∈F∧c∈F→a≤Ib∧b≤Ic→a≤Ic
28 3 4 5 10 18 27 isposd ⊢F∈V→I∈Poset
29 fvprc ⊢¬F∈V→toInc⁡F=∅
30 1 29 eqtrid ⊢¬F∈V→I=∅
31 0pos ⊢∅∈Poset
32 30 31 eqeltrdi ⊢¬F∈V→I∈Poset
33 28 32 pm2.61i ⊢I∈Poset