Metamath Proof Explorer

Theorem elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Hypotheses elovmporab.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M | φ
elovmporab.v ⊢ X ∈ V ∧ Y ∈ V → M ∈ V
Assertion elovmporab ⊢ Z ∈ X O Y → X ∈ V ∧ Y ∈ V ∧ Z ∈ M

Proof

Step Hyp Ref Expression
1 elovmporab.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M | φ
2 elovmporab.v ⊢ X ∈ V ∧ Y ∈ V → M ∈ V
3 1 elmpocl ⊢ Z ∈ X O Y → X ∈ V ∧ Y ∈ V
4 1 a1i ⊢ X ∈ V ∧ Y ∈ V → O = x ∈ V , y ∈ V ⟼ z ∈ M | φ
5 sbceq1a ⊢ y = Y → φ ↔ [˙Y / y]˙ φ
6 sbceq1a ⊢ x = X → [˙Y / y]˙ φ ↔ [˙X / x]˙ [˙Y / y]˙ φ
7 5 6 sylan9bbr ⊢ x = X ∧ y = Y → φ ↔ [˙X / x]˙ [˙Y / y]˙ φ
8 7 adantl ⊢ X ∈ V ∧ Y ∈ V ∧ x = X ∧ y = Y → φ ↔ [˙X / x]˙ [˙Y / y]˙ φ
9 8 rabbidv ⊢ X ∈ V ∧ Y ∈ V ∧ x = X ∧ y = Y → z ∈ M | φ = z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ
10 eqidd ⊢ X ∈ V ∧ Y ∈ V ∧ x = X → V = V
11 simpl ⊢ X ∈ V ∧ Y ∈ V → X ∈ V
12 simpr ⊢ X ∈ V ∧ Y ∈ V → Y ∈ V
13 rabexg ⊢ M ∈ V → z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ ∈ V
14 2 13 syl ⊢ X ∈ V ∧ Y ∈ V → z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ ∈ V
15 nfcv ⊢ Ⅎ _ x X
16 15 nfel1 ⊢ Ⅎ x X ∈ V
17 nfcv ⊢ Ⅎ _ x Y
18 17 nfel1 ⊢ Ⅎ x Y ∈ V
19 16 18 nfan ⊢ Ⅎ x X ∈ V ∧ Y ∈ V
20 nfcv ⊢ Ⅎ _ y X
21 20 nfel1 ⊢ Ⅎ y X ∈ V
22 nfcv ⊢ Ⅎ _ y Y
23 22 nfel1 ⊢ Ⅎ y Y ∈ V
24 21 23 nfan ⊢ Ⅎ y X ∈ V ∧ Y ∈ V
25 nfsbc1v ⊢ Ⅎ x [˙X / x]˙ [˙Y / y]˙ φ
26 nfcv ⊢ Ⅎ _ x M
27 25 26 nfrabw ⊢ Ⅎ _ x z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ
28 nfsbc1v ⊢ Ⅎ y [˙Y / y]˙ φ
29 20 28 nfsbcw ⊢ Ⅎ y [˙X / x]˙ [˙Y / y]˙ φ
30 nfcv ⊢ Ⅎ _ y M
31 29 30 nfrabw ⊢ Ⅎ _ y z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ
32 4 9 10 11 12 14 19 24 20 17 27 31 ovmpodxf ⊢ X ∈ V ∧ Y ∈ V → X O Y = z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ
33 32 eleq2d ⊢ X ∈ V ∧ Y ∈ V → Z ∈ X O Y ↔ Z ∈ z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ
34 df-3an ⊢ X ∈ V ∧ Y ∈ V ∧ Z ∈ M ↔ X ∈ V ∧ Y ∈ V ∧ Z ∈ M
35 34 simplbi2com ⊢ Z ∈ M → X ∈ V ∧ Y ∈ V → X ∈ V ∧ Y ∈ V ∧ Z ∈ M
36 elrabi ⊢ Z ∈ z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ → Z ∈ M
37 35 36 syl11 ⊢ X ∈ V ∧ Y ∈ V → Z ∈ z ∈ M | [˙X / x]˙ [˙Y / y]˙ φ → X ∈ V ∧ Y ∈ V ∧ Z ∈ M
38 33 37 sylbid ⊢ X ∈ V ∧ Y ∈ V → Z ∈ X O Y → X ∈ V ∧ Y ∈ V ∧ Z ∈ M
39 3 38 mpcom ⊢ Z ∈ X O Y → X ∈ V ∧ Y ∈ V ∧ Z ∈ M