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 M$
	enp1i.2	$⊢ N = suc M$
	enp1i.3	$⊢ (A ∖ \{x\}) \approx M \to φ$
	enp1i.4	$⊢ x \in A \to (φ \to ψ)$
Assertion	enp1i	$⊢ A \approx N \to \exists x ψ$

Proof

Step	Hyp	Ref	Expression
1		enp1i.1	$⊢ Ord M$
2		enp1i.2	$⊢ N = suc M$
3		enp1i.3	$⊢ (A ∖ \{x\}) \approx M \to φ$
4		enp1i.4	$⊢ x \in A \to (φ \to ψ)$
5	2	breq2i	$⊢ A \approx N \leftrightarrow A \approx suc M$
6		encv	$⊢ A \approx suc M \to (A \in V \land suc M \in V)$
7	6	simprd	$⊢ A \approx suc M \to suc M \in V$
8		sssucid	$⊢ M \subseteq suc M$
9		ssexg	$⊢ (M \subseteq suc M \land suc M \in V) \to M \in V$
10	8 9	mpan	$⊢ suc M \in V \to M \in V$
11		elong	$⊢ M \in V \to (M \in On \leftrightarrow Ord M)$
12	7 10 11	3syl	$⊢ A \approx suc M \to (M \in On \leftrightarrow Ord M)$
13	1 12	mpbiri	$⊢ A \approx suc M \to M \in On$
14		rexdif1en	$⊢ (M \in On \land A \approx suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$
15	13 14	mpancom	$⊢ A \approx suc M \to \exists x \in A (A ∖ \{x\}) \approx M$
16	3	reximi	$⊢ \exists x \in A (A ∖ \{x\}) \approx M \to \exists x \in A φ$
17		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
18	4	imp	$⊢ (x \in A \land φ) \to ψ$
19	18	eximi	$⊢ \exists x (x \in A \land φ) \to \exists x ψ$
20	17 19	sylbi	$⊢ \exists x \in A φ \to \exists x ψ$
21	15 16 20	3syl	$⊢ A \approx suc M \to \exists x ψ$
22	5 21	sylbi	$⊢ A \approx N \to \exists x ψ$

Metamath Proof Explorer

Theorem enp1i

Proof