This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 )