Metamath Proof Explorer

Theorem inf3lemc

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

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 inf3lemc ⊢ A ∈ ω → F ⁡ suc ⁡ A = G ⁡ F ⁡ A

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 frsuc ⊢ A ∈ ω → rec ⁡ G ∅ ↾ ω ⁡ suc ⁡ A = G ⁡ rec ⁡ G ∅ ↾ ω ⁡ A
6 2 fveq1i ⊢ F ⁡ suc ⁡ A = rec ⁡ G ∅ ↾ ω ⁡ suc ⁡ A
7 2 fveq1i ⊢ F ⁡ A = rec ⁡ G ∅ ↾ ω ⁡ A
8 7 fveq2i ⊢ G ⁡ F ⁡ A = G ⁡ rec ⁡ G ∅ ↾ ω ⁡ A
9 5 6 8 3eqtr4g ⊢ A ∈ ω → F ⁡ suc ⁡ A = G ⁡ F ⁡ A