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 𝑀 ) → ∃ 𝑥𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )