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

Metamath Proof Explorer

Theorem 2oconcl

Description: Closure of the pair swapping function on 2o . (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion 2oconcl ( 𝐴 ∈ 2o → ( 1o ∖ 𝐴 ) ∈ 2o )

Proof

Step Hyp Ref Expression
1 elpri ⊢ ( 𝐴 ∈ { ∅ , 1o } → ( 𝐴 = ∅ ∨ 𝐴 = 1o ) )
2 difeq2 ⊢ ( 𝐴 = ∅ → ( 1o ∖ 𝐴 ) = ( 1o ∖ ∅ ) )
3 dif0 ⊢ ( 1o ∖ ∅ ) = 1o
4 2 3 eqtrdi ⊢ ( 𝐴 = ∅ → ( 1o ∖ 𝐴 ) = 1o )
5 difeq2 ⊢ ( 𝐴 = 1o → ( 1o ∖ 𝐴 ) = ( 1o ∖ 1o ) )
6 difid ⊢ ( 1o ∖ 1o ) = ∅
7 5 6 eqtrdi ⊢ ( 𝐴 = 1o → ( 1o ∖ 𝐴 ) = ∅ )
8 4 7 orim12i ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = 1o ) → ( ( 1o ∖ 𝐴 ) = 1o ∨ ( 1o ∖ 𝐴 ) = ∅ ) )
9 8 orcomd ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = 1o ) → ( ( 1o ∖ 𝐴 ) = ∅ ∨ ( 1o ∖ 𝐴 ) = 1o ) )
10 1 9 syl ⊢ ( 𝐴 ∈ { ∅ , 1o } → ( ( 1o ∖ 𝐴 ) = ∅ ∨ ( 1o ∖ 𝐴 ) = 1o ) )
11 1on ⊢ 1o ∈ On
12 difexg ⊢ ( 1o ∈ On → ( 1o ∖ 𝐴 ) ∈ V )
13 11 12 ax-mp ⊢ ( 1o ∖ 𝐴 ) ∈ V
14 13 elpr ⊢ ( ( 1o ∖ 𝐴 ) ∈ { ∅ , 1o } ↔ ( ( 1o ∖ 𝐴 ) = ∅ ∨ ( 1o ∖ 𝐴 ) = 1o ) )
15 10 14 sylibr ⊢ ( 𝐴 ∈ { ∅ , 1o } → ( 1o ∖ 𝐴 ) ∈ { ∅ , 1o } )
16 df2o3 ⊢ 2o = { ∅ , 1o }
17 15 16 eleqtrrdi ⊢ ( 𝐴 ∈ { ∅ , 1o } → ( 1o ∖ 𝐴 ) ∈ 2o )
18 17 16 eleq2s ⊢ ( 𝐴 ∈ 2o → ( 1o ∖ 𝐴 ) ∈ 2o )