inf3lem7

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex . (Contributed by NM, 29-Oct-1996) (Proof shortened by Mario Carneiro, 19-Jan-2013)

	Ref	Expression
Hypotheses	inf3lem.1	$⊢ G = (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\})$
	inf3lem.2	$⊢ F = {rec (G, \emptyset) ↾}_{ω}$
	inf3lem.3	$⊢ A \in V$
	inf3lem.4	$⊢ B \in V$
Assertion	inf3lem7	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ω \in V$

Proof

Step	Hyp	Ref	Expression
1		inf3lem.1	$⊢ G = (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\})$
2		inf3lem.2	$⊢ F = {rec (G, \emptyset) ↾}_{ω}$
3		inf3lem.3	$⊢ A \in V$
4		inf3lem.4	$⊢ B \in V$
5	1 2 3 4	inf3lem6	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to F : ω \underset{1-1}{⟶} 𝒫 x$
6		vpwex	$⊢ 𝒫 x \in V$
7		f1dmex	$⊢ (F : ω \underset{1-1}{⟶} 𝒫 x \land 𝒫 x \in V) \to ω \in V$
8	5 6 7	sylancl	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ω \in V$

Metamath Proof Explorer

Theorem inf3lem7

Proof