Metamath Proof Explorer

Theorem inf3lemd

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 inf3lemd ⊢ A ∈ ω → F ⁡ A ⊆ x

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 fveq2 ⊢ A = ∅ → F ⁡ A = F ⁡ ∅
6 1 2 3 4 inf3lemb ⊢ F ⁡ ∅ = ∅
7 5 6 eqtrdi ⊢ A = ∅ → F ⁡ A = ∅
8 0ss ⊢ ∅ ⊆ x
9 7 8 eqsstrdi ⊢ A = ∅ → F ⁡ A ⊆ x
10 9 a1d ⊢ A = ∅ → A ∈ ω → F ⁡ A ⊆ x
11 nnsuc ⊢ A ∈ ω ∧ A ≠ ∅ → ∃ v ∈ ω A = suc ⁡ v
12 vex ⊢ v ∈ V
13 1 2 12 4 inf3lemc ⊢ v ∈ ω → F ⁡ suc ⁡ v = G ⁡ F ⁡ v
14 13 eleq2d ⊢ v ∈ ω → u ∈ F ⁡ suc ⁡ v ↔ u ∈ G ⁡ F ⁡ v
15 vex ⊢ u ∈ V
16 fvex ⊢ F ⁡ v ∈ V
17 1 2 15 16 inf3lema ⊢ u ∈ G ⁡ F ⁡ v ↔ u ∈ x ∧ u ∩ x ⊆ F ⁡ v
18 17 simplbi ⊢ u ∈ G ⁡ F ⁡ v → u ∈ x
19 14 18 biimtrdi ⊢ v ∈ ω → u ∈ F ⁡ suc ⁡ v → u ∈ x
20 19 ssrdv ⊢ v ∈ ω → F ⁡ suc ⁡ v ⊆ x
21 fveq2 ⊢ A = suc ⁡ v → F ⁡ A = F ⁡ suc ⁡ v
22 21 sseq1d ⊢ A = suc ⁡ v → F ⁡ A ⊆ x ↔ F ⁡ suc ⁡ v ⊆ x
23 20 22 syl5ibrcom ⊢ v ∈ ω → A = suc ⁡ v → F ⁡ A ⊆ x
24 23 rexlimiv ⊢ ∃ v ∈ ω A = suc ⁡ v → F ⁡ A ⊆ x
25 11 24 syl ⊢ A ∈ ω ∧ A ≠ ∅ → F ⁡ A ⊆ x
26 25 expcom ⊢ A ≠ ∅ → A ∈ ω → F ⁡ A ⊆ x
27 10 26 pm2.61ine ⊢ A ∈ ω → F ⁡ A ⊆ x