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

Metamath Proof Explorer

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 ) → ∪ ( 𝑃 ∖ { ∪ ( 𝑃 ∖ { 𝑋 } ) } ) = 𝑋 )