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