Theorem ensucne0OLD

Description: A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ensucne0OLD	⊢ ( 𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		encv	⊢ ( 𝐴 ≈ suc 𝐵 → ( 𝐴 ∈ V ∧ suc 𝐵 ∈ V ) )
2	1	simprd	⊢ ( 𝐴 ≈ suc 𝐵 → suc 𝐵 ∈ V )
3		en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
4	3	biimpri	⊢ ( 𝐴 = ∅ → 𝐴 ≈ ∅ )
5	4	a1i	⊢ ( suc 𝐵 ∈ V → ( 𝐴 = ∅ → 𝐴 ≈ ∅ ) )
6		nsuceq0	⊢ suc 𝐵 ≠ ∅
7		0sdomg	⊢ ( suc 𝐵 ∈ V → ( ∅ ≺ suc 𝐵 ↔ suc 𝐵 ≠ ∅ ) )
8	6 7	mpbiri	⊢ ( suc 𝐵 ∈ V → ∅ ≺ suc 𝐵 )
9	5 8	jctird	⊢ ( suc 𝐵 ∈ V → ( 𝐴 = ∅ → ( 𝐴 ≈ ∅ ∧ ∅ ≺ suc 𝐵 ) ) )
10		ensdomtr	⊢ ( ( 𝐴 ≈ ∅ ∧ ∅ ≺ suc 𝐵 ) → 𝐴 ≺ suc 𝐵 )
11		sdomnen	⊢ ( 𝐴 ≺ suc 𝐵 → ¬ 𝐴 ≈ suc 𝐵 )
12	10 11	syl	⊢ ( ( 𝐴 ≈ ∅ ∧ ∅ ≺ suc 𝐵 ) → ¬ 𝐴 ≈ suc 𝐵 )
13	9 12	syl6	⊢ ( suc 𝐵 ∈ V → ( 𝐴 = ∅ → ¬ 𝐴 ≈ suc 𝐵 ) )
14	13	necon2ad	⊢ ( suc 𝐵 ∈ V → ( 𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅ ) )
15	2 14	mpcom	⊢ ( 𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅ )