Metamath Proof Explorer

Theorem rexdif1en

Description: If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024) Generalize to all ordinals and avoid ax-un . (Revised by BTernaryTau, 5-Jan-2025)

Ref Expression
Assertion rexdif1en ( ( 𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )

Proof

Step Hyp Ref Expression
1 encv ⊢ ( 𝐴 ≈ suc 𝑀 → ( 𝐴 ∈ V ∧ suc 𝑀 ∈ V ) )
2 1 simpld ⊢ ( 𝐴 ≈ suc 𝑀 → 𝐴 ∈ V )
3 breng ⊢ ( ( 𝐴 ∈ V ∧ suc 𝑀 ∈ V ) → ( 𝐴 ≈ suc 𝑀 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) )
4 1 3 syl ⊢ ( 𝐴 ≈ suc 𝑀 → ( 𝐴 ≈ suc 𝑀 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) )
5 4 ibi ⊢ ( 𝐴 ≈ suc 𝑀 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 )
6 sucidg ⊢ ( 𝑀 ∈ On → 𝑀 ∈ suc 𝑀 )
7 f1ocnvdm ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
8 7 ancoms ⊢ ( ( 𝑀 ∈ suc 𝑀 ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
9 6 8 sylan ⊢ ( ( 𝑀 ∈ On ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
10 9 adantll ⊢ ( ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
11 vex ⊢ 𝑓 ∈ V
12 dif1enlem ⊢ ( ( ( 𝑓 ∈ V ∧ 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 )
13 11 12 mp3anl1 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 )
14 sneq ⊢ ( 𝑥 = ( ◡ 𝑓 ‘ 𝑀 ) → { 𝑥 } = { ( ◡ 𝑓 ‘ 𝑀 ) } )
15 14 difeq2d ⊢ ( 𝑥 = ( ◡ 𝑓 ‘ 𝑀 ) → ( 𝐴 ∖ { 𝑥 } ) = ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) )
16 15 breq1d ⊢ ( 𝑥 = ( ◡ 𝑓 ‘ 𝑀 ) → ( ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ↔ ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 ) )
17 16 rspcev ⊢ ( ( ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 ∧ ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
18 10 13 17 syl2anc ⊢ ( ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
19 18 ex ⊢ ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) → ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ) )
20 19 exlimdv ⊢ ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ) )
21 5 20 syl5 ⊢ ( ( 𝐴 ∈ V ∧ 𝑀 ∈ On ) → ( 𝐴 ≈ suc 𝑀 → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ) )
22 2 21 sylan ⊢ ( ( 𝐴 ≈ suc 𝑀 ∧ 𝑀 ∈ On ) → ( 𝐴 ≈ suc 𝑀 → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ) )
23 22 ancoms ⊢ ( ( 𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ) → ( 𝐴 ≈ suc 𝑀 → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ) )
24 23 syldbl2 ⊢ ( ( 𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )