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 ⊢ F = x ∈ A , y ∈ B ⟼ C
Assertion mpoexxg ⊢ A ∈ R ∧ ∀ x ∈ A B ∈ S → F ∈ V

Proof

Step Hyp Ref Expression
1 mpoexg.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 1 mpofun ⊢ Fun ⁡ F
3 1 dmmpossx ⊢ dom ⁡ F ⊆ ⋃ x ∈ A x × B
4 vsnex ⊢ x ∈ V
5 xpexg ⊢ x ∈ V ∧ B ∈ S → x × B ∈ V
6 4 5 mpan ⊢ B ∈ S → x × B ∈ V
7 6 ralimi ⊢ ∀ x ∈ A B ∈ S → ∀ x ∈ A x × B ∈ V
8 iunexg ⊢ A ∈ R ∧ ∀ x ∈ A x × B ∈ V → ⋃ x ∈ A x × B ∈ V
9 7 8 sylan2 ⊢ A ∈ R ∧ ∀ x ∈ A B ∈ S → ⋃ x ∈ A x × B ∈ V
10 ssexg ⊢ dom ⁡ F ⊆ ⋃ x ∈ A x × B ∧ ⋃ x ∈ A x × B ∈ V → dom ⁡ F ∈ V
11 3 9 10 sylancr ⊢ A ∈ R ∧ ∀ x ∈ A B ∈ S → dom ⁡ F ∈ V
12 funex ⊢ Fun ⁡ F ∧ dom ⁡ F ∈ V → F ∈ V
13 2 11 12 sylancr ⊢ A ∈ R ∧ ∀ x ∈ A B ∈ S → F ∈ V