Metamath Proof Explorer

Theorem 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 ∈ V ⟼ w ∈ x | w ∩ x ⊆ y
inf3lem.2 ⊢ F = rec ⁡ G ∅ ↾ ω
inf3lem.3 ⊢ A ∈ V
inf3lem.4 ⊢ B ∈ V
Assertion inf3lem7 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → ω ∈ V

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ G = y ∈ V ⟼ w ∈ x | w ∩ x ⊆ y
2 inf3lem.2 ⊢ F = rec ⁡ G ∅ ↾ ω
3 inf3lem.3 ⊢ A ∈ V
4 inf3lem.4 ⊢ B ∈ V
5 1 2 3 4 inf3lem6 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → F : ω ⟶ 1-1 𝒫 x
6 vpwex ⊢ 𝒫 x ∈ V
7 f1dmex ⊢ F : ω ⟶ 1-1 𝒫 x ∧ 𝒫 x ∈ V → ω ∈ V
8 5 6 7 sylancl ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → ω ∈ V