This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inf3lema

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 inf3lema ⊢ A ∈ G ⁡ B ↔ A ∈ x ∧ A ∩ x ⊆ B

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 ineq1 ⊢ f = A → f ∩ x = A ∩ x
6 5 sseq1d ⊢ f = A → f ∩ x ⊆ B ↔ A ∩ x ⊆ B
7 sseq2 ⊢ v = B → f ∩ x ⊆ v ↔ f ∩ x ⊆ B
8 7 rabbidv ⊢ v = B → f ∈ x | f ∩ x ⊆ v = f ∈ x | f ∩ x ⊆ B
9 sseq2 ⊢ y = v → w ∩ x ⊆ y ↔ w ∩ x ⊆ v
10 9 rabbidv ⊢ y = v → w ∈ x | w ∩ x ⊆ y = w ∈ x | w ∩ x ⊆ v
11 ineq1 ⊢ w = f → w ∩ x = f ∩ x
12 11 sseq1d ⊢ w = f → w ∩ x ⊆ v ↔ f ∩ x ⊆ v
13 12 cbvrabv ⊢ w ∈ x | w ∩ x ⊆ v = f ∈ x | f ∩ x ⊆ v
14 10 13 eqtrdi ⊢ y = v → w ∈ x | w ∩ x ⊆ y = f ∈ x | f ∩ x ⊆ v
15 14 cbvmptv ⊢ y ∈ V ⟼ w ∈ x | w ∩ x ⊆ y = v ∈ V ⟼ f ∈ x | f ∩ x ⊆ v
16 1 15 eqtri ⊢ G = v ∈ V ⟼ f ∈ x | f ∩ x ⊆ v
17 vex ⊢ x ∈ V
18 17 rabex ⊢ f ∈ x | f ∩ x ⊆ B ∈ V
19 8 16 18 fvmpt ⊢ B ∈ V → G ⁡ B = f ∈ x | f ∩ x ⊆ B
20 4 19 ax-mp ⊢ G ⁡ B = f ∈ x | f ∩ x ⊆ B
21 6 20 elrab2 ⊢ A ∈ G ⁡ B ↔ A ∈ x ∧ A ∩ x ⊆ B