Proof of Theorem ovi3
Step | Hyp | Ref
| Expression |
1 | | ovi3.1 |
. . . 4
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻)) |
2 | | elex 2741 |
. . . 4
⊢ (𝑆 ∈ (𝐻 × 𝐻) → 𝑆 ∈ V) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ V) |
4 | | isset 2736 |
. . 3
⊢ (𝑆 ∈ V ↔ ∃𝑧 𝑧 = 𝑆) |
5 | 3, 4 | sylib 121 |
. 2
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → ∃𝑧 𝑧 = 𝑆) |
6 | | nfv 1521 |
. . 3
⊢
Ⅎ𝑧((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) |
7 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑧〈𝐴, 𝐵〉 |
8 | | ovi3.3 |
. . . . . 6
⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} |
9 | | nfoprab3 5902 |
. . . . . 6
⊢
Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} |
10 | 8, 9 | nfcxfr 2309 |
. . . . 5
⊢
Ⅎ𝑧𝐹 |
11 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑧〈𝐶, 𝐷〉 |
12 | 7, 10, 11 | nfov 5881 |
. . . 4
⊢
Ⅎ𝑧(〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) |
13 | 12 | nfeq1 2322 |
. . 3
⊢
Ⅎ𝑧(〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆 |
14 | | ovi3.2 |
. . . . . . 7
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆) |
15 | 14 | eqeq2d 2182 |
. . . . . 6
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (𝑧 = 𝑅 ↔ 𝑧 = 𝑆)) |
16 | 15 | copsex4g 4230 |
. . . . 5
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ 𝑧 = 𝑆)) |
17 | | opelxpi 4641 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → 〈𝐴, 𝐵〉 ∈ (𝐻 × 𝐻)) |
18 | | opelxpi 4641 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻) → 〈𝐶, 𝐷〉 ∈ (𝐻 × 𝐻)) |
19 | | nfcv 2312 |
. . . . . . 7
⊢
Ⅎ𝑥〈𝐴, 𝐵〉 |
20 | | nfcv 2312 |
. . . . . . 7
⊢
Ⅎ𝑦〈𝐴, 𝐵〉 |
21 | | nfcv 2312 |
. . . . . . 7
⊢
Ⅎ𝑦〈𝐶, 𝐷〉 |
22 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) |
23 | | nfoprab1 5900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} |
24 | 8, 23 | nfcxfr 2309 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
25 | | nfcv 2312 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 |
26 | 19, 24, 25 | nfov 5881 |
. . . . . . . . 9
⊢
Ⅎ𝑥(〈𝐴, 𝐵〉𝐹𝑦) |
27 | 26 | nfeq1 2322 |
. . . . . . . 8
⊢
Ⅎ𝑥(〈𝐴, 𝐵〉𝐹𝑦) = 𝑧 |
28 | 22, 27 | nfim 1565 |
. . . . . . 7
⊢
Ⅎ𝑥(∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹𝑦) = 𝑧) |
29 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑦∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) |
30 | | nfoprab2 5901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} |
31 | 8, 30 | nfcxfr 2309 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐹 |
32 | 20, 31, 21 | nfov 5881 |
. . . . . . . . 9
⊢
Ⅎ𝑦(〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) |
33 | 32 | nfeq1 2322 |
. . . . . . . 8
⊢
Ⅎ𝑦(〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧 |
34 | 29, 33 | nfim 1565 |
. . . . . . 7
⊢
Ⅎ𝑦(∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧) |
35 | | eqeq1 2177 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑥 = 〈𝑤, 𝑣〉 ↔ 〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉)) |
36 | 35 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ↔ (〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉))) |
37 | 36 | anbi1d 462 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))) |
38 | 37 | 4exbidv 1863 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))) |
39 | | oveq1 5858 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑥𝐹𝑦) = (〈𝐴, 𝐵〉𝐹𝑦)) |
40 | 39 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((𝑥𝐹𝑦) = 𝑧 ↔ (〈𝐴, 𝐵〉𝐹𝑦) = 𝑧)) |
41 | 38, 40 | imbi12d 233 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (𝑥𝐹𝑦) = 𝑧) ↔ (∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹𝑦) = 𝑧))) |
42 | | eqeq1 2177 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (𝑦 = 〈𝑢, 𝑓〉 ↔ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉)) |
43 | 42 | anbi2d 461 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝐶, 𝐷〉 → ((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ↔ (〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉))) |
44 | 43 | anbi1d 462 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))) |
45 | 44 | 4exbidv 1863 |
. . . . . . . 8
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))) |
46 | | oveq2 5859 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (〈𝐴, 𝐵〉𝐹𝑦) = (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉)) |
47 | 46 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑦 = 〈𝐶, 𝐷〉 → ((〈𝐴, 𝐵〉𝐹𝑦) = 𝑧 ↔ (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧)) |
48 | 45, 47 | imbi12d 233 |
. . . . . . 7
⊢ (𝑦 = 〈𝐶, 𝐷〉 → ((∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹𝑦) = 𝑧) ↔ (∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧))) |
49 | | moeq 2905 |
. . . . . . . . . . . 12
⊢
∃*𝑧 𝑧 = 𝑅 |
50 | 49 | mosubop 4675 |
. . . . . . . . . . 11
⊢
∃*𝑧∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅) |
51 | 50 | mosubop 4675 |
. . . . . . . . . 10
⊢
∃*𝑧∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅)) |
52 | | anass 399 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅))) |
53 | 52 | 2exbii 1599 |
. . . . . . . . . . . . 13
⊢
(∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ∃𝑢∃𝑓(𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅))) |
54 | | 19.42vv 1904 |
. . . . . . . . . . . . 13
⊢
(∃𝑢∃𝑓(𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅)) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅))) |
55 | 53, 54 | bitri 183 |
. . . . . . . . . . . 12
⊢
(∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅))) |
56 | 55 | 2exbii 1599 |
. . . . . . . . . . 11
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅))) |
57 | 56 | mobii 2056 |
. . . . . . . . . 10
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) ↔ ∃*𝑧∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 𝑅))) |
58 | 51, 57 | mpbir 145 |
. . . . . . . . 9
⊢
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) |
59 | 58 | a1i 9 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅)) |
60 | 59, 8 | ovidi 5969 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) → (∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (𝑥𝐹𝑦) = 𝑧)) |
61 | 19, 20, 21, 28, 34, 41, 48, 60 | vtocl2gaf 2797 |
. . . . . 6
⊢
((〈𝐴, 𝐵〉 ∈ (𝐻 × 𝐻) ∧ 〈𝐶, 𝐷〉 ∈ (𝐻 × 𝐻)) → (∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧)) |
62 | 17, 18, 61 | syl2an 287 |
. . . . 5
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃𝑤∃𝑣∃𝑢∃𝑓((〈𝐴, 𝐵〉 = 〈𝑤, 𝑣〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧)) |
63 | 16, 62 | sylbird 169 |
. . . 4
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (𝑧 = 𝑆 → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧)) |
64 | | eqeq2 2180 |
. . . 4
⊢ (𝑧 = 𝑆 → ((〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑧 ↔ (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆)) |
65 | 63, 64 | mpbidi 150 |
. . 3
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (𝑧 = 𝑆 → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆)) |
66 | 6, 13, 65 | exlimd 1590 |
. 2
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃𝑧 𝑧 = 𝑆 → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆)) |
67 | 5, 66 | mpd 13 |
1
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆) |