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

Metamath Proof Explorer

Theorem zfcndinf

Description: Axiom of Infinity ax-inf , reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003)

Ref Expression
Assertion zfcndinf ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y

Proof

Step Hyp Ref Expression
1 el ⊢ ∃ w x ∈ w
2 nfv ⊢ Ⅎ w x ∈ y
3 nfe1 ⊢ Ⅎ w ∃ w x ∈ w ∧ w ∈ y
4 2 3 nfim ⊢ Ⅎ w x ∈ y → ∃ w x ∈ w ∧ w ∈ y
5 4 nfal ⊢ Ⅎ w ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
6 2 5 nfan ⊢ Ⅎ w x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
7 6 nfex ⊢ Ⅎ w ∃ y x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
8 axinfnd ⊢ ∃ y x ∈ w → x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
9 8 19.37iv ⊢ x ∈ w → ∃ y x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
10 7 9 exlimi ⊢ ∃ w x ∈ w → ∃ y x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
11 1 10 ax-mp ⊢ ∃ y x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
12 elequ1 ⊢ z = x → z ∈ y ↔ x ∈ y
13 elequ1 ⊢ z = x → z ∈ w ↔ x ∈ w
14 13 anbi1d ⊢ z = x → z ∈ w ∧ w ∈ y ↔ x ∈ w ∧ w ∈ y
15 14 exbidv ⊢ z = x → ∃ w z ∈ w ∧ w ∈ y ↔ ∃ w x ∈ w ∧ w ∈ y
16 12 15 imbi12d ⊢ z = x → z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ x ∈ y → ∃ w x ∈ w ∧ w ∈ y
17 16 cbvalvw ⊢ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
18 17 anbi2i ⊢ x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
19 18 exbii ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ ∃ y x ∈ y ∧ ∀ x x ∈ y → ∃ w x ∈ w ∧ w ∈ y
20 11 19 mpbir ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y