Metamath Proof Explorer


Theorem enp1i

Description: Proof induction for en2 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016) Generalize to all ordinals and avoid ax-pow , ax-un . (Revised by BTernaryTau, 6-Jan-2025)

Ref Expression
Hypotheses enp1i.1 Ord 𝑀
enp1i.2 𝑁 = suc 𝑀
enp1i.3 ( ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀𝜑 )
enp1i.4 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
Assertion enp1i ( 𝐴𝑁 → ∃ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 enp1i.1 Ord 𝑀
2 enp1i.2 𝑁 = suc 𝑀
3 enp1i.3 ( ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀𝜑 )
4 enp1i.4 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
5 2 breq2i ( 𝐴𝑁𝐴 ≈ suc 𝑀 )
6 encv ( 𝐴 ≈ suc 𝑀 → ( 𝐴 ∈ V ∧ suc 𝑀 ∈ V ) )
7 6 simprd ( 𝐴 ≈ suc 𝑀 → suc 𝑀 ∈ V )
8 sssucid 𝑀 ⊆ suc 𝑀
9 ssexg ( ( 𝑀 ⊆ suc 𝑀 ∧ suc 𝑀 ∈ V ) → 𝑀 ∈ V )
10 8 9 mpan ( suc 𝑀 ∈ V → 𝑀 ∈ V )
11 elong ( 𝑀 ∈ V → ( 𝑀 ∈ On ↔ Ord 𝑀 ) )
12 7 10 11 3syl ( 𝐴 ≈ suc 𝑀 → ( 𝑀 ∈ On ↔ Ord 𝑀 ) )
13 1 12 mpbiri ( 𝐴 ≈ suc 𝑀𝑀 ∈ On )
14 rexdif1en ( ( 𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ) → ∃ 𝑥𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
15 13 14 mpancom ( 𝐴 ≈ suc 𝑀 → ∃ 𝑥𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
16 3 reximi ( ∃ 𝑥𝐴 ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 → ∃ 𝑥𝐴 𝜑 )
17 df-rex ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐴𝜑 ) )
18 4 imp ( ( 𝑥𝐴𝜑 ) → 𝜓 )
19 18 eximi ( ∃ 𝑥 ( 𝑥𝐴𝜑 ) → ∃ 𝑥 𝜓 )
20 17 19 sylbi ( ∃ 𝑥𝐴 𝜑 → ∃ 𝑥 𝜓 )
21 15 16 20 3syl ( 𝐴 ≈ suc 𝑀 → ∃ 𝑥 𝜓 )
22 5 21 sylbi ( 𝐴𝑁 → ∃ 𝑥 𝜓 )