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

Metamath Proof Explorer

Theorem inf3lem4

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-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 inf3lem4 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → A ∈ ω → F ⁡ A ⊂ F ⁡ suc ⁡ 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 1 2 3 4 inf3lem1 ⊢ A ∈ ω → F ⁡ A ⊆ F ⁡ suc ⁡ A
6 5 a1i ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → A ∈ ω → F ⁡ A ⊆ F ⁡ suc ⁡ A
7 1 2 3 4 inf3lem3 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → A ∈ ω → F ⁡ A ≠ F ⁡ suc ⁡ A
8 6 7 jcad ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → A ∈ ω → F ⁡ A ⊆ F ⁡ suc ⁡ A ∧ F ⁡ A ≠ F ⁡ suc ⁡ A
9 df-pss ⊢ F ⁡ A ⊂ F ⁡ suc ⁡ A ↔ F ⁡ A ⊆ F ⁡ suc ⁡ A ∧ F ⁡ A ≠ F ⁡ suc ⁡ A
10 8 9 imbitrrdi ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → A ∈ ω → F ⁡ A ⊂ F ⁡ suc ⁡ A