MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ov3 Structured version   Visualization version   GIF version

Theorem ov3 6995
Description: The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
Hypotheses
Ref Expression
ov3.1 𝑆 ∈ V
ov3.2 (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → 𝑅 = 𝑆)
ov3.3 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
Assertion
Ref Expression
ov3 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆)
Distinct variable groups:   𝑢,𝑓,𝑣,𝑤,𝑥,𝑦,𝑧,𝐴   𝐵,𝑓,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝐶,𝑓,𝑢,𝑣,𝑤,𝑦,𝑧   𝐷,𝑓,𝑢,𝑣,𝑤,𝑦,𝑧   𝑓,𝐻,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧   𝑆,𝑓,𝑢,𝑣,𝑤,𝑧
Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑥)   𝑅(𝑤,𝑣,𝑢,𝑓)   𝑆(𝑥,𝑦)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓)

Proof of Theorem ov3
StepHypRef Expression
1 ov3.1 . . 3 𝑆 ∈ V
21isseti 3362 . 2 𝑧 𝑧 = 𝑆
3 nfv 2009 . . 3 𝑧((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻))
4 nfcv 2907 . . . . 5 𝑧𝐴, 𝐵
5 ov3.3 . . . . . 6 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
6 nfoprab3 6904 . . . . . 6 𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
75, 6nfcxfr 2905 . . . . 5 𝑧𝐹
8 nfcv 2907 . . . . 5 𝑧𝐶, 𝐷
94, 7, 8nfov 6872 . . . 4 𝑧(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩)
109nfeq1 2921 . . 3 𝑧(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆
11 ov3.2 . . . . . . 7 (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → 𝑅 = 𝑆)
1211eqeq2d 2775 . . . . . 6 (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → (𝑧 = 𝑅𝑧 = 𝑆))
1312copsex4g 5114 . . . . 5 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ 𝑧 = 𝑆))
14 opelxpi 5314 . . . . . 6 ((𝐴𝐻𝐵𝐻) → ⟨𝐴, 𝐵⟩ ∈ (𝐻 × 𝐻))
15 opelxpi 5314 . . . . . 6 ((𝐶𝐻𝐷𝐻) → ⟨𝐶, 𝐷⟩ ∈ (𝐻 × 𝐻))
16 nfcv 2907 . . . . . . 7 𝑥𝐴, 𝐵
17 nfcv 2907 . . . . . . 7 𝑦𝐴, 𝐵
18 nfcv 2907 . . . . . . 7 𝑦𝐶, 𝐷
19 nfv 2009 . . . . . . . 8 𝑥𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)
20 nfoprab1 6902 . . . . . . . . . . 11 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
215, 20nfcxfr 2905 . . . . . . . . . 10 𝑥𝐹
22 nfcv 2907 . . . . . . . . . 10 𝑥𝑦
2316, 21, 22nfov 6872 . . . . . . . . 9 𝑥(⟨𝐴, 𝐵𝐹𝑦)
2423nfeq1 2921 . . . . . . . 8 𝑥(⟨𝐴, 𝐵𝐹𝑦) = 𝑧
2519, 24nfim 1995 . . . . . . 7 𝑥(∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝑦) = 𝑧)
26 nfv 2009 . . . . . . . 8 𝑦𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)
27 nfoprab2 6903 . . . . . . . . . . 11 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
285, 27nfcxfr 2905 . . . . . . . . . 10 𝑦𝐹
2917, 28, 18nfov 6872 . . . . . . . . 9 𝑦(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩)
3029nfeq1 2921 . . . . . . . 8 𝑦(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧
3126, 30nfim 1995 . . . . . . 7 𝑦(∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧)
32 eqeq1 2769 . . . . . . . . . . 11 (𝑥 = ⟨𝐴, 𝐵⟩ → (𝑥 = ⟨𝑤, 𝑣⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩))
3332anbi1d 623 . . . . . . . . . 10 (𝑥 = ⟨𝐴, 𝐵⟩ → ((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩)))
3433anbi1d 623 . . . . . . . . 9 (𝑥 = ⟨𝐴, 𝐵⟩ → (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
35344exbidv 2021 . . . . . . . 8 (𝑥 = ⟨𝐴, 𝐵⟩ → (∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
36 oveq1 6849 . . . . . . . . 9 (𝑥 = ⟨𝐴, 𝐵⟩ → (𝑥𝐹𝑦) = (⟨𝐴, 𝐵𝐹𝑦))
3736eqeq1d 2767 . . . . . . . 8 (𝑥 = ⟨𝐴, 𝐵⟩ → ((𝑥𝐹𝑦) = 𝑧 ↔ (⟨𝐴, 𝐵𝐹𝑦) = 𝑧))
3835, 37imbi12d 335 . . . . . . 7 (𝑥 = ⟨𝐴, 𝐵⟩ → ((∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (𝑥𝐹𝑦) = 𝑧) ↔ (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝑦) = 𝑧)))
39 eqeq1 2769 . . . . . . . . . . 11 (𝑦 = ⟨𝐶, 𝐷⟩ → (𝑦 = ⟨𝑢, 𝑓⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩))
4039anbi2d 622 . . . . . . . . . 10 (𝑦 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩)))
4140anbi1d 623 . . . . . . . . 9 (𝑦 = ⟨𝐶, 𝐷⟩ → (((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
42414exbidv 2021 . . . . . . . 8 (𝑦 = ⟨𝐶, 𝐷⟩ → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
43 oveq2 6850 . . . . . . . . 9 (𝑦 = ⟨𝐶, 𝐷⟩ → (⟨𝐴, 𝐵𝐹𝑦) = (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩))
4443eqeq1d 2767 . . . . . . . 8 (𝑦 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵𝐹𝑦) = 𝑧 ↔ (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
4542, 44imbi12d 335 . . . . . . 7 (𝑦 = ⟨𝐶, 𝐷⟩ → ((∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝑦) = 𝑧) ↔ (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧)))
46 moeq 3535 . . . . . . . . . . . 12 ∃*𝑧 𝑧 = 𝑅
4746mosubop 5132 . . . . . . . . . . 11 ∃*𝑧𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)
4847mosubop 5132 . . . . . . . . . 10 ∃*𝑧𝑤𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅))
49 anass 460 . . . . . . . . . . . . . 14 (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
50492exbii 1944 . . . . . . . . . . . . 13 (∃𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑢𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
51 19.42vv 2050 . . . . . . . . . . . . 13 (∃𝑢𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
5250, 51bitri 266 . . . . . . . . . . . 12 (∃𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
53522exbii 1944 . . . . . . . . . . 11 (∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑤𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
5453mobii 2568 . . . . . . . . . 10 (∃*𝑧𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃*𝑧𝑤𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
5548, 54mpbir 222 . . . . . . . . 9 ∃*𝑧𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)
5655a1i 11 . . . . . . . 8 ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) → ∃*𝑧𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))
5756, 5ovidi 6977 . . . . . . 7 ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) → (∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (𝑥𝐹𝑦) = 𝑧))
5816, 17, 18, 25, 31, 38, 45, 57vtocl2gaf 3425 . . . . . 6 ((⟨𝐴, 𝐵⟩ ∈ (𝐻 × 𝐻) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝐻 × 𝐻)) → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
5914, 15, 58syl2an 589 . . . . 5 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
6013, 59sylbird 251 . . . 4 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (𝑧 = 𝑆 → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
61 eqeq2 2776 . . . 4 (𝑧 = 𝑆 → ((⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧 ↔ (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆))
6260, 61mpbidi 232 . . 3 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (𝑧 = 𝑆 → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆))
633, 10, 62exlimd 2251 . 2 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (∃𝑧 𝑧 = 𝑆 → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆))
642, 63mpi 20 1 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wex 1874  wcel 2155  ∃*wmo 2563  Vcvv 3350  cop 4340   × cxp 5275  (class class class)co 6842  {coprab 6843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-iota 6031  df-fun 6070  df-fv 6076  df-ov 6845  df-oprab 6846
This theorem is referenced by:  addcnsr  10209  mulcnsr  10210
  Copyright terms: Public domain W3C validator