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 ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑧 ∈ V
2 1 cplem2 ⊢ ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ( { 𝑦 ∣ 𝜑 } ≠ ∅ → ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ≠ ∅ )
3 abn0 ⊢ ( { 𝑦 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑦 𝜑 )
4 elin ⊢ ( 𝑦 ∈ ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ↔ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑤 ) )
5 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
6 5 anbi1i ⊢ ( ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑤 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝑤 ) )
7 ancom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑤 ) ↔ ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) )
8 4 6 7 3bitri ⊢ ( 𝑦 ∈ ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ↔ ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) )
9 8 exbii ⊢ ( ∃ 𝑦 𝑦 ∈ ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) )
10 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
11 nfcv ⊢ Ⅎ 𝑦 𝑤
12 10 11 nfin ⊢ Ⅎ 𝑦 ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 )
13 12 n0f ⊢ ( ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) )
14 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑤 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) )
15 9 13 14 3bitr4i ⊢ ( ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑤 𝜑 )
16 3 15 imbi12i ⊢ ( ( { 𝑦 ∣ 𝜑 } ≠ ∅ → ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ≠ ∅ ) ↔ ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
17 16 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑧 ( { 𝑦 ∣ 𝜑 } ≠ ∅ → ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
18 17 exbii ⊢ ( ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ( { 𝑦 ∣ 𝜑 } ≠ ∅ → ( { 𝑦 ∣ 𝜑 } ∩ 𝑤 ) ≠ ∅ ) ↔ ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
19 2 18 mpbi ⊢ ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 )