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
|- ( A e. 2o -> ( 1o \ A ) e. 2o )

Proof

Step Hyp Ref Expression
1 elpri
 |-  ( A e. { (/) , 1o } -> ( A = (/) \/ A = 1o ) )
2 difeq2
 |-  ( A = (/) -> ( 1o \ A ) = ( 1o \ (/) ) )
3 dif0
 |-  ( 1o \ (/) ) = 1o
4 2 3 eqtrdi
 |-  ( A = (/) -> ( 1o \ A ) = 1o )
5 difeq2
 |-  ( A = 1o -> ( 1o \ A ) = ( 1o \ 1o ) )
6 difid
 |-  ( 1o \ 1o ) = (/)
7 5 6 eqtrdi
 |-  ( A = 1o -> ( 1o \ A ) = (/) )
8 4 7 orim12i
 |-  ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = 1o \/ ( 1o \ A ) = (/) ) )
9 8 orcomd
 |-  ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
10 1 9 syl
 |-  ( A e. { (/) , 1o } -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
11 1on
 |-  1o e. On
12 difexg
 |-  ( 1o e. On -> ( 1o \ A ) e. _V )
13 11 12 ax-mp
 |-  ( 1o \ A ) e. _V
14 13 elpr
 |-  ( ( 1o \ A ) e. { (/) , 1o } <-> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
15 10 14 sylibr
 |-  ( A e. { (/) , 1o } -> ( 1o \ A ) e. { (/) , 1o } )
16 df2o3
 |-  2o = { (/) , 1o }
17 15 16 eleqtrrdi
 |-  ( A e. { (/) , 1o } -> ( 1o \ A ) e. 2o )
18 17 16 eleq2s
 |-  ( A e. 2o -> ( 1o \ A ) e. 2o )