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

Metamath Proof Explorer

Theorem cp

Description: Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick scottex that collapses a proper class into a set of minimum rank. The wff ph can be thought of as ph ( x , y ) . Scheme "Collection Principle" of Jech p. 72. (Contributed by NM, 17-Oct-2003)

Ref Expression
Assertion cp ⊢ ∃ w ∀ x ∈ z ∃ y φ → ∃ y ∈ w φ

Proof

Step Hyp Ref Expression
1 vex ⊢ z ∈ V
2 1 cplem2 ⊢ ∃ w ∀ x ∈ z y | φ ≠ ∅ → y | φ ∩ w ≠ ∅
3 abn0 ⊢ y | φ ≠ ∅ ↔ ∃ y φ
4 elin ⊢ y ∈ y | φ ∩ w ↔ y ∈ y | φ ∧ y ∈ w
5 abid ⊢ y ∈ y | φ ↔ φ
6 5 anbi1i ⊢ y ∈ y | φ ∧ y ∈ w ↔ φ ∧ y ∈ w
7 ancom ⊢ φ ∧ y ∈ w ↔ y ∈ w ∧ φ
8 4 6 7 3bitri ⊢ y ∈ y | φ ∩ w ↔ y ∈ w ∧ φ
9 8 exbii ⊢ ∃ y y ∈ y | φ ∩ w ↔ ∃ y y ∈ w ∧ φ
10 nfab1 ⊢ Ⅎ _ y y | φ
11 nfcv ⊢ Ⅎ _ y w
12 10 11 nfin ⊢ Ⅎ _ y y | φ ∩ w
13 12 n0f ⊢ y | φ ∩ w ≠ ∅ ↔ ∃ y y ∈ y | φ ∩ w
14 df-rex ⊢ ∃ y ∈ w φ ↔ ∃ y y ∈ w ∧ φ
15 9 13 14 3bitr4i ⊢ y | φ ∩ w ≠ ∅ ↔ ∃ y ∈ w φ
16 3 15 imbi12i ⊢ y | φ ≠ ∅ → y | φ ∩ w ≠ ∅ ↔ ∃ y φ → ∃ y ∈ w φ
17 16 ralbii ⊢ ∀ x ∈ z y | φ ≠ ∅ → y | φ ∩ w ≠ ∅ ↔ ∀ x ∈ z ∃ y φ → ∃ y ∈ w φ
18 17 exbii ⊢ ∃ w ∀ x ∈ z y | φ ≠ ∅ → y | φ ∩ w ≠ ∅ ↔ ∃ w ∀ x ∈ z ∃ y φ → ∃ y ∈ w φ
19 2 18 mpbi ⊢ ∃ w ∀ x ∈ z ∃ y φ → ∃ y ∈ w φ