Metamath Proof Explorer

Theorem dif1en

Description: If a set A is equinumerous to the successor of a natural number M , then A with an element removed is equinumerous to M . For a proof with fewer symbols using ax-pow , see dif1enALT . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024)

Ref Expression
Assertion dif1en ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ suc 𝑀 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 )
2 19.41v ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ) )
3 3anass ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ↔ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ) )
4 3 exbii ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ↔ ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ) )
5 3anass ⊢ ( ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ) )
6 2 4 5 3bitr4i ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) )
7 sucidg ⊢ ( 𝑀 ∈ ω → 𝑀 ∈ suc 𝑀 )
8 f1ocnvdm ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
9 8 3adant2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
10 f1ofvswap ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
11 9 10 syld3an3 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
12 f1ocnvfv2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) = 𝑀 )
13 12 opeq2d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ = ⟨ 𝑋 , 𝑀 ⟩ )
14 13 preq1d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } = { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } )
15 14 uneq2d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) = ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) )
16 15 f1oeq1d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ↔ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) )
17 16 3adant2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ↔ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) )
18 11 17 mpbid ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
19 f1ofun ⊢ ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 → Fun ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) )
20 opex ⊢ ⟨ 𝑋 , 𝑀 ⟩ ∈ V
21 20 prid1 ⊢ ⟨ 𝑋 , 𝑀 ⟩ ∈ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ }
22 elun2 ⊢ ( ⟨ 𝑋 , 𝑀 ⟩ ∈ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } → ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) )
23 21 22 ax-mp ⊢ ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } )
24 funopfv ⊢ ( Fun ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) → ( ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 ) )
25 23 24 mpi ⊢ ( Fun ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 )
26 18 19 25 3syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 )
27 simp2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → 𝑋 ∈ 𝐴 )
28 f1ocnvfv ⊢ ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 ) )
29 18 27 28 syl2anc ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 ) )
30 26 29 mpd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 )
31 7 30 syl3an3 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 )
32 31 sneqd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } = { 𝑋 } )
33 32 difeq2d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) = ( 𝐴 ∖ { 𝑋 } ) )
34 vex ⊢ 𝑓 ∈ V
35 34 resex ⊢ ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∈ V
36 prex ⊢ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ∈ V
37 35 36 unex ⊢ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ∈ V
38 simp3 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → 𝑀 ∈ ω )
39 7 18 syl3an3 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
40 dif1enlem ⊢ ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ∈ V ∧ 𝑀 ∈ ω ∧ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) ≈ 𝑀 )
41 37 38 39 40 mp3an2i ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) ≈ 𝑀 )
42 33 41 eqbrtrrd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
43 42 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
44 6 43 sylbir ⊢ ( ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
45 1 44 syl3an1b ⊢ ( ( 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
46 45 3comr ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )