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