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

Metamath Proof Explorer

Theorem mpoexxg

Description: Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypothesis mpoexg.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion mpoexxg ( ( 𝐴 ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 mpoexg.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 1 mpofun ⊢ Fun 𝐹
3 1 dmmpossx ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
4 vsnex ⊢ { 𝑥 } ∈ V
5 xpexg ⊢ ( ( { 𝑥 } ∈ V ∧ 𝐵 ∈ 𝑆 ) → ( { 𝑥 } × 𝐵 ) ∈ V )
6 4 5 mpan ⊢ ( 𝐵 ∈ 𝑆 → ( { 𝑥 } × 𝐵 ) ∈ V )
7 6 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 → ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ V )
8 iunexg ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ V )
9 7 8 sylan2 ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ V )
10 ssexg ⊢ ( ( dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ V ) → dom 𝐹 ∈ V )
11 3 9 10 sylancr ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ) → dom 𝐹 ∈ V )
12 funex ⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ V ) → 𝐹 ∈ V )
13 2 11 12 sylancr ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ) → 𝐹 ∈ V )