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

Metamath Proof Explorer

Theorem unidifsnne

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

Ref Expression
Assertion unidifsnne ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 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 simplll ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → 𝑋 ∈ 𝑃 )
26 25 elexd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → 𝑋 ∈ V )
27 simplr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
28 sneqbg ⊢ ( 𝑋 ∈ 𝑃 → ( { 𝑋 } = { 𝑥 } ↔ 𝑋 = 𝑥 ) )
29 28 biimpar ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑋 = 𝑥 ) → { 𝑋 } = { 𝑥 } )
30 29 ad4ant14 ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → { 𝑋 } = { 𝑥 } )
31 27 30 eqtr4d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑋 } )
32 31 ineq2d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( { 𝑋 } ∩ ( 𝑃 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∩ { 𝑋 } ) )
33 disjdif ⊢ ( { 𝑋 } ∩ ( 𝑃 ∖ { 𝑋 } ) ) = ∅
34 inidm ⊢ ( { 𝑋 } ∩ { 𝑋 } ) = { 𝑋 }
35 32 33 34 3eqtr3g ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ∅ = { 𝑋 } )
36 35 eqcomd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → { 𝑋 } = ∅ )
37 snprc ⊢ ( ¬ 𝑋 ∈ V ↔ { 𝑋 } = ∅ )
38 36 37 sylibr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ¬ 𝑋 ∈ V )
39 26 38 pm2.65da ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ¬ 𝑋 = 𝑥 )
40 39 neqned ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑋 ≠ 𝑥 )
41 simpr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
42 41 unieqd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = ∪ { 𝑥 } )
43 unisnv ⊢ ∪ { 𝑥 } = 𝑥
44 42 43 eqtrdi ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = 𝑥 )
45 40 44 neeqtrrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑋 ≠ ∪ ( 𝑃 ∖ { 𝑋 } ) )
46 45 necomd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )
47 24 46 exlimddv ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )