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 )