Theorem enrefnn

Description: Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg ). (Contributed by BTernaryTau, 31-Jul-2024)

	Ref	Expression
Assertion	enrefnn	⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
2	1 1	breq12d	⊢ ( 𝑥 = ∅ → ( 𝑥 ≈ 𝑥 ↔ ∅ ≈ ∅ ) )
3		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
4	3 3	breq12d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑥 ↔ 𝑦 ≈ 𝑦 ) )
5		id	⊢ ( 𝑥 = suc 𝑦 → 𝑥 = suc 𝑦 )
6	5 5	breq12d	⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ≈ 𝑥 ↔ suc 𝑦 ≈ suc 𝑦 ) )
7		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
8	7 7	breq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴 ) )
9		eqid	⊢ ∅ = ∅
10		en0	⊢ ( ∅ ≈ ∅ ↔ ∅ = ∅ )
11	9 10	mpbir	⊢ ∅ ≈ ∅
12		en2sn	⊢ ( ( 𝑦 ∈ V ∧ 𝑦 ∈ V ) → { 𝑦 } ≈ { 𝑦 } )
13	12	el2v	⊢ { 𝑦 } ≈ { 𝑦 }
14	13	jctr	⊢ ( 𝑦 ≈ 𝑦 → ( 𝑦 ≈ 𝑦 ∧ { 𝑦 } ≈ { 𝑦 } ) )
15		nnord	⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
16		orddisj	⊢ ( Ord 𝑦 → ( 𝑦 ∩ { 𝑦 } ) = ∅ )
17	15 16	syl	⊢ ( 𝑦 ∈ ω → ( 𝑦 ∩ { 𝑦 } ) = ∅ )
18	17 17	jca	⊢ ( 𝑦 ∈ ω → ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ∧ ( 𝑦 ∩ { 𝑦 } ) = ∅ ) )
19		unen	⊢ ( ( ( 𝑦 ≈ 𝑦 ∧ { 𝑦 } ≈ { 𝑦 } ) ∧ ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ∧ ( 𝑦 ∩ { 𝑦 } ) = ∅ ) ) → ( 𝑦 ∪ { 𝑦 } ) ≈ ( 𝑦 ∪ { 𝑦 } ) )
20	14 18 19	syl2anr	⊢ ( ( 𝑦 ∈ ω ∧ 𝑦 ≈ 𝑦 ) → ( 𝑦 ∪ { 𝑦 } ) ≈ ( 𝑦 ∪ { 𝑦 } ) )
21		df-suc	⊢ suc 𝑦 = ( 𝑦 ∪ { 𝑦 } )
22	20 21 21	3brtr4g	⊢ ( ( 𝑦 ∈ ω ∧ 𝑦 ≈ 𝑦 ) → suc 𝑦 ≈ suc 𝑦 )
23	22	ex	⊢ ( 𝑦 ∈ ω → ( 𝑦 ≈ 𝑦 → suc 𝑦 ≈ suc 𝑦 ) )
24	2 4 6 8 11 23	finds	⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 )