Theorem mpoexxg2

Description: Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpoexxg . (Contributed by AV, 30-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mpoexxg2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	mpofun	⊢ Fun 𝐹
3	1	dmmpossx2	⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } )
4		snex	⊢ { 𝑦 } ∈ V
5		xpexg	⊢ ( ( 𝐴 ∈ 𝑆 ∧ { 𝑦 } ∈ V ) → ( 𝐴 × { 𝑦 } ) ∈ V )
6	4 5	mpan2	⊢ ( 𝐴 ∈ 𝑆 → ( 𝐴 × { 𝑦 } ) ∈ 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 )