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 )