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

Metamath Proof Explorer

Theorem hashrabrex

Description: The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018)

Ref Expression
Hypotheses hashrabrex.1 ⊢ ( 𝜑 → 𝑌 ∈ Fin )
hashrabrex.2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → { 𝑥 ∈ 𝑋 ∣ 𝜓 } ∈ Fin )
hashrabrex.3 ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ 𝜓 } )
Assertion hashrabrex ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 𝜓 } ) = Σ 𝑦 ∈ 𝑌 ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ 𝜓 } ) )

Proof

Step Hyp Ref Expression
1 hashrabrex.1 ⊢ ( 𝜑 → 𝑌 ∈ Fin )
2 hashrabrex.2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → { 𝑥 ∈ 𝑋 ∣ 𝜓 } ∈ Fin )
3 hashrabrex.3 ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ 𝜓 } )
4 iunrab ⊢ ∪ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ 𝜓 } = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 𝜓 }
5 4 eqcomi ⊢ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 𝜓 } = ∪ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ 𝜓 }
6 5 fveq2i ⊢ ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 𝜓 } ) = ( ♯ ‘ ∪ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ 𝜓 } )
7 1 2 3 hashiun ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ 𝜓 } ) = Σ 𝑦 ∈ 𝑌 ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ 𝜓 } ) )
8 6 7 eqtrid ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 𝜓 } ) = Σ 𝑦 ∈ 𝑌 ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ 𝜓 } ) )