Metamath Proof Explorer

Theorem ovmpt3rab1

Description: The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

Ref Expression
Hypotheses ovmpt3rab1.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M ⟼ a ∈ N | φ
ovmpt3rab1.m ⊢ x = X ∧ y = Y → M = K
ovmpt3rab1.n ⊢ x = X ∧ y = Y → N = L
ovmpt3rab1.p ⊢ x = X ∧ y = Y → φ ↔ ψ
ovmpt3rab1.x ⊢ Ⅎ x ψ
ovmpt3rab1.y ⊢ Ⅎ y ψ
Assertion ovmpt3rab1 ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U → X O Y = z ∈ K ⟼ a ∈ L | ψ

Proof

Step Hyp Ref Expression
1 ovmpt3rab1.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M ⟼ a ∈ N | φ
2 ovmpt3rab1.m ⊢ x = X ∧ y = Y → M = K
3 ovmpt3rab1.n ⊢ x = X ∧ y = Y → N = L
4 ovmpt3rab1.p ⊢ x = X ∧ y = Y → φ ↔ ψ
5 ovmpt3rab1.x ⊢ Ⅎ x ψ
6 ovmpt3rab1.y ⊢ Ⅎ y ψ
7 1 a1i ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U → O = x ∈ V , y ∈ V ⟼ z ∈ M ⟼ a ∈ N | φ
8 3 4 rabeqbidv ⊢ x = X ∧ y = Y → a ∈ N | φ = a ∈ L | ψ
9 2 8 mpteq12dv ⊢ x = X ∧ y = Y → z ∈ M ⟼ a ∈ N | φ = z ∈ K ⟼ a ∈ L | ψ
10 9 adantl ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U ∧ x = X ∧ y = Y → z ∈ M ⟼ a ∈ N | φ = z ∈ K ⟼ a ∈ L | ψ
11 eqidd ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U ∧ x = X → V = V
12 elex ⊢ X ∈ V → X ∈ V
13 12 3ad2ant1 ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U → X ∈ V
14 elex ⊢ Y ∈ W → Y ∈ V
15 14 3ad2ant2 ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U → Y ∈ V
16 mptexg ⊢ K ∈ U → z ∈ K ⟼ a ∈ L | ψ ∈ V
17 16 3ad2ant3 ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U → z ∈ K ⟼ a ∈ L | ψ ∈ V
18 nfv ⊢ Ⅎ x X ∈ V ∧ Y ∈ W ∧ K ∈ U
19 nfv ⊢ Ⅎ y X ∈ V ∧ Y ∈ W ∧ K ∈ U
20 nfcv ⊢ Ⅎ _ y X
21 nfcv ⊢ Ⅎ _ x Y
22 nfcv ⊢ Ⅎ _ x K
23 nfcv ⊢ Ⅎ _ x L
24 5 23 nfrabw ⊢ Ⅎ _ x a ∈ L | ψ
25 22 24 nfmpt ⊢ Ⅎ _ x z ∈ K ⟼ a ∈ L | ψ
26 nfcv ⊢ Ⅎ _ y K
27 nfcv ⊢ Ⅎ _ y L
28 6 27 nfrabw ⊢ Ⅎ _ y a ∈ L | ψ
29 26 28 nfmpt ⊢ Ⅎ _ y z ∈ K ⟼ a ∈ L | ψ
30 7 10 11 13 15 17 18 19 20 21 25 29 ovmpodxf ⊢ X ∈ V ∧ Y ∈ W ∧ K ∈ U → X O Y = z ∈ K ⟼ a ∈ L | ψ