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

Metamath Proof Explorer

Theorem unidifsnel

Description: The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 2onn ⊢ 2o ∈ ω
2 nnfi ⊢ ( 2o ∈ ω → 2o ∈ Fin )
3 1 2 ax-mp ⊢ 2o ∈ Fin
4 enfi ⊢ ( 𝑃 ≈ 2o → ( 𝑃 ∈ Fin ↔ 2o ∈ Fin ) )
5 3 4 mpbiri ⊢ ( 𝑃 ≈ 2o → 𝑃 ∈ Fin )
6 5 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 ∈ Fin )
7 diffi ⊢ ( 𝑃 ∈ Fin → ( 𝑃 ∖ { 𝑋 } ) ∈ Fin )
8 6 7 syl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ∈ Fin )
9 8 cardidd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) ≈ ( 𝑃 ∖ { 𝑋 } ) )
10 9 ensymd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ≈ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) )
11 simpl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑋 ∈ 𝑃 )
12 dif1card ⊢ ( ( 𝑃 ∈ Fin ∧ 𝑋 ∈ 𝑃 ) → ( card ‘ 𝑃 ) = suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) )
13 6 11 12 syl2anc ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ 𝑃 ) = suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) )
14 cardennn ⊢ ( ( 𝑃 ≈ 2o ∧ 2o ∈ ω ) → ( card ‘ 𝑃 ) = 2o )
15 1 14 mpan2 ⊢ ( 𝑃 ≈ 2o → ( card ‘ 𝑃 ) = 2o )
16 df-2o ⊢ 2o = suc 1o
17 15 16 eqtrdi ⊢ ( 𝑃 ≈ 2o → ( card ‘ 𝑃 ) = suc 1o )
18 17 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ 𝑃 ) = suc 1o )
19 13 18 eqtr3d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = suc 1o )
20 suc11reg ⊢ ( suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = suc 1o ↔ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o )
21 19 20 sylib ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o )
22 10 21 breqtrd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ≈ 1o )
23 en1 ⊢ ( ( 𝑃 ∖ { 𝑋 } ) ≈ 1o ↔ ∃ 𝑥 ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
24 22 23 sylib ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∃ 𝑥 ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
25 simpr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
26 25 unieqd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = ∪ { 𝑥 } )
27 unisnv ⊢ ∪ { 𝑥 } = 𝑥
28 26 27 eqtrdi ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = 𝑥 )
29 difssd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) ⊆ 𝑃 )
30 25 29 eqsstrrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → { 𝑥 } ⊆ 𝑃 )
31 vsnid ⊢ 𝑥 ∈ { 𝑥 }
32 ssel2 ⊢ ( ( { 𝑥 } ⊆ 𝑃 ∧ 𝑥 ∈ { 𝑥 } ) → 𝑥 ∈ 𝑃 )
33 30 31 32 sylancl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑥 ∈ 𝑃 )
34 28 33 eqeltrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ 𝑃 )
35 24 34 exlimddv ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ 𝑃 )