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

Theorem ov3 7304
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 3513 . 2 𝑧 𝑧 = 𝑆
3 nfv 1908 . . 3 𝑧((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻))
4 nfcv 2981 . . . . 5 𝑧𝐴, 𝐵
5 ov3.3 . . . . . 6 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
6 nfoprab3 7212 . . . . . 6 𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
75, 6nfcxfr 2979 . . . . 5 𝑧𝐹
8 nfcv 2981 . . . . 5 𝑧𝐶, 𝐷
94, 7, 8nfov 7181 . . . 4 𝑧(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩)
109nfeq1 2997 . . 3 𝑧(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆
11 ov3.2 . . . . . . 7 (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → 𝑅 = 𝑆)
1211eqeq2d 2836 . . . . . 6 (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → (𝑧 = 𝑅𝑧 = 𝑆))
1312copsex4g 5381 . . . . 5 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ 𝑧 = 𝑆))
14 opelxpi 5590 . . . . . 6 ((𝐴𝐻𝐵𝐻) → ⟨𝐴, 𝐵⟩ ∈ (𝐻 × 𝐻))
15 opelxpi 5590 . . . . . 6 ((𝐶𝐻𝐷𝐻) → ⟨𝐶, 𝐷⟩ ∈ (𝐻 × 𝐻))
16 nfcv 2981 . . . . . . 7 𝑥𝐴, 𝐵
17 nfcv 2981 . . . . . . 7 𝑦𝐴, 𝐵
18 nfcv 2981 . . . . . . 7 𝑦𝐶, 𝐷
19 nfv 1908 . . . . . . . 8 𝑥𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)
20 nfoprab1 7210 . . . . . . . . . . 11 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
215, 20nfcxfr 2979 . . . . . . . . . 10 𝑥𝐹
22 nfcv 2981 . . . . . . . . . 10 𝑥𝑦
2316, 21, 22nfov 7181 . . . . . . . . 9 𝑥(⟨𝐴, 𝐵𝐹𝑦)
2423nfeq1 2997 . . . . . . . 8 𝑥(⟨𝐴, 𝐵𝐹𝑦) = 𝑧
2519, 24nfim 1890 . . . . . . 7 𝑥(∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝑦) = 𝑧)
26 nfv 1908 . . . . . . . 8 𝑦𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)
27 nfoprab2 7211 . . . . . . . . . . 11 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}
285, 27nfcxfr 2979 . . . . . . . . . 10 𝑦𝐹
2917, 28, 18nfov 7181 . . . . . . . . 9 𝑦(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩)
3029nfeq1 2997 . . . . . . . 8 𝑦(⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧
3126, 30nfim 1890 . . . . . . 7 𝑦(∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧)
32 eqeq1 2829 . . . . . . . . . . 11 (𝑥 = ⟨𝐴, 𝐵⟩ → (𝑥 = ⟨𝑤, 𝑣⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩))
3332anbi1d 629 . . . . . . . . . 10 (𝑥 = ⟨𝐴, 𝐵⟩ → ((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩)))
3433anbi1d 629 . . . . . . . . 9 (𝑥 = ⟨𝐴, 𝐵⟩ → (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
35344exbidv 1920 . . . . . . . 8 (𝑥 = ⟨𝐴, 𝐵⟩ → (∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
36 oveq1 7158 . . . . . . . . 9 (𝑥 = ⟨𝐴, 𝐵⟩ → (𝑥𝐹𝑦) = (⟨𝐴, 𝐵𝐹𝑦))
3736eqeq1d 2827 . . . . . . . 8 (𝑥 = ⟨𝐴, 𝐵⟩ → ((𝑥𝐹𝑦) = 𝑧 ↔ (⟨𝐴, 𝐵𝐹𝑦) = 𝑧))
3835, 37imbi12d 346 . . . . . . 7 (𝑥 = ⟨𝐴, 𝐵⟩ → ((∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (𝑥𝐹𝑦) = 𝑧) ↔ (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝑦) = 𝑧)))
39 eqeq1 2829 . . . . . . . . . . 11 (𝑦 = ⟨𝐶, 𝐷⟩ → (𝑦 = ⟨𝑢, 𝑓⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩))
4039anbi2d 628 . . . . . . . . . 10 (𝑦 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩)))
4140anbi1d 629 . . . . . . . . 9 (𝑦 = ⟨𝐶, 𝐷⟩ → (((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
42414exbidv 1920 . . . . . . . 8 (𝑦 = ⟨𝐶, 𝐷⟩ → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)))
43 oveq2 7159 . . . . . . . . 9 (𝑦 = ⟨𝐶, 𝐷⟩ → (⟨𝐴, 𝐵𝐹𝑦) = (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩))
4443eqeq1d 2827 . . . . . . . 8 (𝑦 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵𝐹𝑦) = 𝑧 ↔ (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
4542, 44imbi12d 346 . . . . . . 7 (𝑦 = ⟨𝐶, 𝐷⟩ → ((∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝑦) = 𝑧) ↔ (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧)))
46 moeq 3701 . . . . . . . . . . . 12 ∃*𝑧 𝑧 = 𝑅
4746mosubop 5397 . . . . . . . . . . 11 ∃*𝑧𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)
4847mosubop 5397 . . . . . . . . . 10 ∃*𝑧𝑤𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅))
49 anass 469 . . . . . . . . . . . . . 14 (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
50492exbii 1842 . . . . . . . . . . . . 13 (∃𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑢𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
51 19.42vv 1951 . . . . . . . . . . . . 13 (∃𝑢𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
5250, 51bitri 276 . . . . . . . . . . . 12 (∃𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
53522exbii 1842 . . . . . . . . . . 11 (∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃𝑤𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
5453mobii 2628 . . . . . . . . . 10 (∃*𝑧𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) ↔ ∃*𝑧𝑤𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = 𝑅)))
5548, 54mpbir 232 . . . . . . . . 9 ∃*𝑧𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅)
5655a1i 11 . . . . . . . 8 ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) → ∃*𝑧𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))
5756, 5ovidi 7286 . . . . . . 7 ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) → (∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (𝑥𝐹𝑦) = 𝑧))
5816, 17, 18, 25, 31, 38, 45, 57vtocl2gaf 3580 . . . . . 6 ((⟨𝐴, 𝐵⟩ ∈ (𝐻 × 𝐻) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝐻 × 𝐻)) → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
5914, 15, 58syl2an 595 . . . . 5 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (∃𝑤𝑣𝑢𝑓((⟨𝐴, 𝐵⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
6013, 59sylbird 261 . . . 4 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (𝑧 = 𝑆 → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧))
61 eqeq2 2837 . . . 4 (𝑧 = 𝑆 → ((⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑧 ↔ (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆))
6260, 61mpbidi 242 . . 3 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (𝑧 = 𝑆 → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆))
633, 10, 62exlimd 2211 . 2 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (∃𝑧 𝑧 = 𝑆 → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆))
642, 63mpi 20 1 (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wex 1773  wcel 2107  ∃*wmo 2617  Vcvv 3499  cop 4569   × cxp 5551  (class class class)co 7151  {coprab 7152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-iota 6311  df-fun 6353  df-fv 6359  df-ov 7154  df-oprab 7155
This theorem is referenced by:  addcnsr  10549  mulcnsr  10550
  Copyright terms: Public domain W3C validator