Metamath Proof Explorer


Theorem cpcoll2d

Description: cpcolld with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 cpcoll2d.1 ( 𝜑𝑥𝐴 )
2 cpcoll2d.2 ( 𝜑 → ∃ 𝑦 𝑥 𝐹 𝑦 )
3 breq2 ( 𝑎 = 𝑦 → ( 𝑥 𝐹 𝑎𝑥 𝐹 𝑦 ) )
4 3 cbvexvw ( ∃ 𝑎 𝑥 𝐹 𝑎 ↔ ∃ 𝑦 𝑥 𝐹 𝑦 )
5 2 4 sylibr ( 𝜑 → ∃ 𝑎 𝑥 𝐹 𝑎 )
6 1 adantr ( ( 𝜑𝑥 𝐹 𝑎 ) → 𝑥𝐴 )
7 simpr ( ( 𝜑𝑥 𝐹 𝑎 ) → 𝑥 𝐹 𝑎 )
8 6 7 cpcolld ( ( 𝜑𝑥 𝐹 𝑎 ) → ∃ 𝑎 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑎 )
9 3 cbvrexvw ( ∃ 𝑎 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑎 ↔ ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 )
10 8 9 sylib ( ( 𝜑𝑥 𝐹 𝑎 ) → ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 )
11 5 10 exlimddv ( 𝜑 → ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 )