Metamath Proof Explorer

Theorem dif1en

Description: If a set A is equinumerous to the successor of an ordinal M , then A with an element removed is equinumerous to M . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → 𝐴 ≈ suc 𝑀 )
2 encv ⊢ ( 𝐴 ≈ suc 𝑀 → ( 𝐴 ∈ V ∧ suc 𝑀 ∈ V ) )
3 2 simpld ⊢ ( 𝐴 ≈ suc 𝑀 → 𝐴 ∈ V )
4 3 3anim1i ⊢ ( ( 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) )
5 bren ⊢ ( 𝐴 ≈ suc 𝑀 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 )
6 sucidg ⊢ ( 𝑀 ∈ On → 𝑀 ∈ suc 𝑀 )
7 f1ocnvdm ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
8 7 3adant2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
9 f1ofvswap ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
10 8 9 syld3an3 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
11 f1ocnvfv2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) = 𝑀 )
12 11 opeq2d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ = ⟨ 𝑋 , 𝑀 ⟩ )
13 12 preq1d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } = { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } )
14 13 uneq2d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) = ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) )
15 14 f1oeq1d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ↔ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) )
16 15 3adant2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑀 ) ) ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ↔ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) )
17 10 16 mpbid ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
18 6 17 syl3an3 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
19 18 3adant3r1 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 )
20 f1ofun ⊢ ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 → Fun ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) )
21 opex ⊢ ⟨ 𝑋 , 𝑀 ⟩ ∈ V
22 21 prid1 ⊢ ⟨ 𝑋 , 𝑀 ⟩ ∈ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ }
23 elun2 ⊢ ( ⟨ 𝑋 , 𝑀 ⟩ ∈ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } → ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) )
24 22 23 ax-mp ⊢ ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } )
25 funopfv ⊢ ( Fun ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) → ( ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 ) )
26 24 25 mpi ⊢ ( Fun ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 )
27 19 20 26 3syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 )
28 simpr2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → 𝑋 ∈ 𝐴 )
29 f1ocnvfv ⊢ ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 ) )
30 19 28 29 syl2anc ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑋 ) = 𝑀 → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 ) )
31 27 30 mpd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) = 𝑋 )
32 31 sneqd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } = { 𝑋 } )
33 32 difeq2d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) = ( 𝐴 ∖ { 𝑋 } ) )
34 simpr1 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → 𝐴 ∈ V )
35 3simpc ⊢ ( ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) )
36 35 anim2i ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) )
37 3anass ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ↔ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) )
38 36 37 sylibr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) )
39 34 38 jca ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝐴 ∈ V ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) )
40 simpl ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → 𝐴 ∈ V )
41 simpr3 ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → 𝑀 ∈ On )
42 40 41 jca ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) )
43 simpr ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) )
44 42 43 jca ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) )
45 vex ⊢ 𝑓 ∈ V
46 45 resex ⊢ ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∈ V
47 prex ⊢ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ∈ V
48 46 47 unex ⊢ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ∈ V
49 dif1enlem ⊢ ( ( ( ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ∈ V ∧ 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) ≈ 𝑀 )
50 48 49 mp3anl1 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) ≈ 𝑀 )
51 18 50 sylan2 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) ≈ 𝑀 )
52 39 44 51 3syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝐴 ∖ { ( ◡ ( ( 𝑓 ↾ ( 𝐴 ∖ { 𝑋 , ( ◡ 𝑓 ‘ 𝑀 ) } ) ) ∪ { ⟨ 𝑋 , 𝑀 ⟩ , ⟨ ( ◡ 𝑓 ‘ 𝑀 ) , ( 𝑓 ‘ 𝑋 ) ⟩ } ) ‘ 𝑀 ) } ) ≈ 𝑀 )
53 33 52 eqbrtrrd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
54 53 ex ⊢ ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 → ( ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ) )
55 54 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 → ( ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ) )
56 5 55 sylbi ⊢ ( 𝐴 ≈ suc 𝑀 → ( ( 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ) )
57 1 4 56 sylc ⊢ ( ( 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
58 57 3comr ⊢ ( ( 𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )