Theorem en2other2

Description: Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Assertion	en2other2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		en2eleq	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 = { 𝑋 , ∪ ( 𝑃 ∖ { 𝑋 } ) } )
2		prcom	⊢ { 𝑋 , ∪ ( 𝑃 ∖ { 𝑋 } ) } = { ∪ ( 𝑃 ∖ { 𝑋 } ) , 𝑋 }
3	1 2	eqtrdi	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 = { ∪ ( 𝑃 ∖ { 𝑋 } ) , 𝑋 } )
4	3	difeq1d	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) = ( { ∪ ( 𝑃 ∖ { 𝑋 } ) , 𝑋 } ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) )
5		difprsnss	⊢ ( { ∪ ( 𝑃 ∖ { 𝑋 } ) , 𝑋 } ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) ⊆ { 𝑋 }
6	4 5	eqsstrdi	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) ⊆ { 𝑋 } )
7		simpl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑋 ∈ 𝑃 )
8		1onn	⊢ 1o ∈ ω
9		simpr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 ≈ 2o )
10		df-2o	⊢ 2o = suc 1o
11	9 10	breqtrdi	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 ≈ suc 1o )
12		dif1ennn	⊢ ( ( 1o ∈ ω ∧ 𝑃 ≈ suc 1o ∧ 𝑋 ∈ 𝑃 ) → ( 𝑃 ∖ { 𝑋 } ) ≈ 1o )
13	8 11 7 12	mp3an2i	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ≈ 1o )
14		en1uniel	⊢ ( ( 𝑃 ∖ { 𝑋 } ) ≈ 1o → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ ( 𝑃 ∖ { 𝑋 } ) )
15		eldifsni	⊢ ( ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ ( 𝑃 ∖ { 𝑋 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )
16	13 14 15	3syl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )
17	16	necomd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑋 ≠ ∪ ( 𝑃 ∖ { 𝑋 } ) )
18		eldifsn	⊢ ( 𝑋 ∈ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) ↔ ( 𝑋 ∈ 𝑃 ∧ 𝑋 ≠ ∪ ( 𝑃 ∖ { 𝑋 } ) ) )
19	7 17 18	sylanbrc	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑋 ∈ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) )
20	19	snssd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → { 𝑋 } ⊆ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) )
21	6 20	eqssd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) = { 𝑋 } )
22	21	unieqd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) = ∪ { 𝑋 } )
23		unisng	⊢ ( 𝑋 ∈ 𝑃 → ∪ { 𝑋 } = 𝑋 )
24	23	adantr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ { 𝑋 } = 𝑋 )
25	22 24	eqtrd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) = 𝑋 )