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 )