Theorem cpcolld

Description: Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	cpcolld.1	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
	cpcolld.2	⊢ ( 𝜑 → 𝑥 𝐹 𝑦 )
Assertion	cpcolld	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		cpcolld.1	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
2		cpcolld.2	⊢ ( 𝜑 → 𝑥 𝐹 𝑦 )
3		vex	⊢ 𝑦 ∈ V
4		breq2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 𝐹 𝑧 ↔ 𝑥 𝐹 𝑦 ) )
5	3 4	elab	⊢ ( 𝑦 ∈ { 𝑧 ∣ 𝑥 𝐹 𝑧 } ↔ 𝑥 𝐹 𝑦 )
6	2 5	sylibr	⊢ ( 𝜑 → 𝑦 ∈ { 𝑧 ∣ 𝑥 𝐹 𝑧 } )
7	6	19.8ad	⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ { 𝑧 ∣ 𝑥 𝐹 𝑧 } )
8	7	scotteld	⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } )
9		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } ⊆ ∪ 𝑥 ∈ 𝐴 Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } )
10		dfcoll2	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 }
11	9 10	sseqtrrdi	⊢ ( 𝑥 ∈ 𝐴 → Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } ⊆ ( 𝐹 Coll 𝐴 ) )
12	11	sselda	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } ) → 𝑦 ∈ ( 𝐹 Coll 𝐴 ) )
13	4	elscottab	⊢ ( 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } → 𝑥 𝐹 𝑦 )
14	13	adantl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } ) → 𝑥 𝐹 𝑦 )
15	12 14	jca	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } ) → ( 𝑦 ∈ ( 𝐹 Coll 𝐴 ) ∧ 𝑥 𝐹 𝑦 ) )
16	15	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } → ( 𝑦 ∈ ( 𝐹 Coll 𝐴 ) ∧ 𝑥 𝐹 𝑦 ) ) )
17	16	eximdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 𝑦 ∈ Scott { 𝑧 ∣ 𝑥 𝐹 𝑧 } → ∃ 𝑦 ( 𝑦 ∈ ( 𝐹 Coll 𝐴 ) ∧ 𝑥 𝐹 𝑦 ) ) )
18	1 8 17	sylc	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ∈ ( 𝐹 Coll 𝐴 ) ∧ 𝑥 𝐹 𝑦 ) )
19		df-rex	⊢ ( ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝐹 Coll 𝐴 ) ∧ 𝑥 𝐹 𝑦 ) )
20	18 19	sylibr	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 )