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 = Base I
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 ≤ I a ↔ a ⊆ a
9 8 3anidm23 ⊢ F ∈ V ∧ a ∈ F → a ≤ I a ↔ a ⊆ a
10 6 9 mpbiri ⊢ F ∈ V ∧ a ∈ F → a ≤ I a
11 1 7 ipole ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F → a ≤ I b ↔ a ⊆ b
12 1 7 ipole ⊢ F ∈ V ∧ b ∈ F ∧ a ∈ F → b ≤ I a ↔ b ⊆ a
13 12 3com23 ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F → b ≤ I a ↔ b ⊆ a
14 11 13 anbi12d ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F → a ≤ I b ∧ b ≤ I a ↔ 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 ≤ I b ∧ b ≤ I a → 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 ≤ I b ↔ a ⊆ b
22 1 7 ipole ⊢ F ∈ V ∧ b ∈ F ∧ c ∈ F → b ≤ I c ↔ b ⊆ c
23 22 3adant3r1 ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F ∧ c ∈ F → b ≤ I c ↔ b ⊆ c
24 21 23 anbi12d ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F ∧ c ∈ F → a ≤ I b ∧ b ≤ I c ↔ a ⊆ b ∧ b ⊆ c
25 1 7 ipole ⊢ F ∈ V ∧ a ∈ F ∧ c ∈ F → a ≤ I c ↔ a ⊆ c
26 25 3adant3r2 ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F ∧ c ∈ F → a ≤ I c ↔ a ⊆ c
27 20 24 26 3imtr4d ⊢ F ∈ V ∧ a ∈ F ∧ b ∈ F ∧ c ∈ F → a ≤ I b ∧ b ≤ I c → a ≤ I c
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