This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( toInc ‘ 𝐹 )
Assertion ipopos 𝐼 ∈ Poset

Proof

Step Hyp Ref Expression
1 ipopos.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 1 fvexi ⊢ 𝐼 ∈ V
3 2 a1i ⊢ ( 𝐹 ∈ V → 𝐼 ∈ V )
4 1 ipobas ⊢ ( 𝐹 ∈ V → 𝐹 = ( Base ‘ 𝐼 ) )
5 eqidd ⊢ ( 𝐹 ∈ V → ( le ‘ 𝐼 ) = ( le ‘ 𝐼 ) )
6 ssid ⊢ 𝑎 ⊆ 𝑎
7 eqid ⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
8 1 7 ipole ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑎 ⊆ 𝑎 ) )
9 8 3anidm23 ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑎 ⊆ 𝑎 ) )
10 6 9 mpbiri ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ) → 𝑎 ( le ‘ 𝐼 ) 𝑎 )
11 1 7 ipole ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ↔ 𝑎 ⊆ 𝑏 ) )
12 1 7 ipole ⊢ ( ( 𝐹 ∈ V ∧ 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑏 ⊆ 𝑎 ) )
13 12 3com23 ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑏 ⊆ 𝑎 ) )
14 11 13 anbi12d ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑎 ) ↔ ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) )
15 simpl ⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) → 𝑎 ⊆ 𝑏 )
16 simpr ⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) → 𝑏 ⊆ 𝑎 )
17 15 16 eqssd ⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) → 𝑎 = 𝑏 )
18 14 17 biimtrdi ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑎 ) → 𝑎 = 𝑏 ) )
19 sstr ⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑐 ) → 𝑎 ⊆ 𝑐 )
20 19 a1i ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑐 ) → 𝑎 ⊆ 𝑐 ) )
21 11 3adant3r3 ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ↔ 𝑎 ⊆ 𝑏 ) )
22 1 7 ipole ⊢ ( ( 𝐹 ∈ V ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑏 ⊆ 𝑐 ) )
23 22 3adant3r1 ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑏 ⊆ 𝑐 ) )
24 21 23 anbi12d ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑐 ) ↔ ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑐 ) ) )
25 1 7 ipole ⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑎 ⊆ 𝑐 ) )
26 25 3adant3r2 ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑎 ⊆ 𝑐 ) )
27 20 24 26 3imtr4d ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑐 ) → 𝑎 ( le ‘ 𝐼 ) 𝑐 ) )
28 3 4 5 10 18 27 isposd ⊢ ( 𝐹 ∈ V → 𝐼 ∈ Poset )
29 fvprc ⊢ ( ¬ 𝐹 ∈ V → ( toInc ‘ 𝐹 ) = ∅ )
30 1 29 eqtrid ⊢ ( ¬ 𝐹 ∈ V → 𝐼 = ∅ )
31 0pos ⊢ ∅ ∈ Poset
32 30 31 eqeltrdi ⊢ ( ¬ 𝐹 ∈ V → 𝐼 ∈ Poset )
33 28 32 pm2.61i ⊢ 𝐼 ∈ Poset