Theorem rexdif1en

Description: If a set is equinumerous to a nonzero finite 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)

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

Proof

Step	Hyp	Ref	Expression
1		bren	⊢ ( 𝐴 ≈ suc 𝑀 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 )
2		19.42v	⊢ ( ∃ 𝑓 ( 𝑀 ∈ ω ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) ↔ ( 𝑀 ∈ ω ∧ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) )
3		sucidg	⊢ ( 𝑀 ∈ ω → 𝑀 ∈ suc 𝑀 )
4		f1ocnvdm	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
5	4	ancoms	⊢ ( ( 𝑀 ∈ suc 𝑀 ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
6	3 5	sylan	⊢ ( ( 𝑀 ∈ ω ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 )
7		vex	⊢ 𝑓 ∈ V
8		dif1enlem	⊢ ( ( 𝑓 ∈ V ∧ 𝑀 ∈ ω ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 )
9	7 8	mp3an1	⊢ ( ( 𝑀 ∈ ω ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 )
10		sneq	⊢ ( 𝑥 = ( ◡ 𝑓 ‘ 𝑀 ) → { 𝑥 } = { ( ◡ 𝑓 ‘ 𝑀 ) } )
11	10	difeq2d	⊢ ( 𝑥 = ( ◡ 𝑓 ‘ 𝑀 ) → ( 𝐴 ∖ { 𝑥 } ) = ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) )
12	11	breq1d	⊢ ( 𝑥 = ( ◡ 𝑓 ‘ 𝑀 ) → ( ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 ↔ ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 ) )
13	12	rspcev	⊢ ( ( ( ◡ 𝑓 ‘ 𝑀 ) ∈ 𝐴 ∧ ( 𝐴 ∖ { ( ◡ 𝑓 ‘ 𝑀 ) } ) ≈ 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
14	6 9 13	syl2anc	⊢ ( ( 𝑀 ∈ ω ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
15	14	exlimiv	⊢ ( ∃ 𝑓 ( 𝑀 ∈ ω ∧ 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
16	2 15	sylbir	⊢ ( ( 𝑀 ∈ ω ∧ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
17	1 16	sylan2b	⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )