Proof of Theorem ovi3
Step | Hyp | Ref
| Expression |
1 | | ovi3.1 |
. . . 4
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻)) |
2 | | elex 2560 |
. . . 4
⊢ (𝑆 ∈ (𝐻 × 𝐻) → 𝑆 ∈
V) |
3 | 1, 2 | syl 14 |
. . 3
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈
V) |
4 | | isset 2555 |
. . 3
⊢ (𝑆 ∈ V ↔ ∃z z = 𝑆) |
5 | 3, 4 | sylib 127 |
. 2
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → ∃z z = 𝑆) |
6 | | nfv 1418 |
. . 3
⊢
Ⅎz((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) |
7 | | nfcv 2175 |
. . . . 5
⊢
Ⅎz〈A, B〉 |
8 | | ovi3.3 |
. . . . . 6
⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 𝑅))} |
9 | | nfoprab3 5498 |
. . . . . 6
⊢
Ⅎz{〈〈x, y〉,
z〉 ∣ ((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 𝑅))} |
10 | 8, 9 | nfcxfr 2172 |
. . . . 5
⊢
Ⅎz𝐹 |
11 | | nfcv 2175 |
. . . . 5
⊢
Ⅎz〈𝐶, 𝐷〉 |
12 | 7, 10, 11 | nfov 5478 |
. . . 4
⊢
Ⅎz(〈A, B〉𝐹〈𝐶, 𝐷〉) |
13 | 12 | nfeq1 2184 |
. . 3
⊢
Ⅎz(〈A, B〉𝐹〈𝐶, 𝐷〉) = 𝑆 |
14 | | ovi3.2 |
. . . . . . 7
⊢
(((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → 𝑅 = 𝑆) |
15 | 14 | eqeq2d 2048 |
. . . . . 6
⊢
(((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → (z = 𝑅 ↔ z = 𝑆)) |
16 | 15 | copsex4g 3975 |
. . . . 5
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅) ↔ z = 𝑆)) |
17 | | opelxpi 4319 |
. . . . . 6
⊢
((A ∈ 𝐻 ∧ B ∈ 𝐻) → 〈A, B〉 ∈ (𝐻 × 𝐻)) |
18 | | opelxpi 4319 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻) → 〈𝐶, 𝐷〉 ∈
(𝐻 × 𝐻)) |
19 | | nfcv 2175 |
. . . . . . 7
⊢
Ⅎx〈A, B〉 |
20 | | nfcv 2175 |
. . . . . . 7
⊢
Ⅎy〈A, B〉 |
21 | | nfcv 2175 |
. . . . . . 7
⊢
Ⅎy〈𝐶, 𝐷〉 |
22 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎx∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅) |
23 | | nfoprab1 5496 |
. . . . . . . . . . 11
⊢
Ⅎx{〈〈x, y〉,
z〉 ∣ ((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 𝑅))} |
24 | 8, 23 | nfcxfr 2172 |
. . . . . . . . . 10
⊢
Ⅎx𝐹 |
25 | | nfcv 2175 |
. . . . . . . . . 10
⊢
Ⅎxy |
26 | 19, 24, 25 | nfov 5478 |
. . . . . . . . 9
⊢
Ⅎx(〈A, B〉𝐹y) |
27 | 26 | nfeq1 2184 |
. . . . . . . 8
⊢
Ⅎx(〈A, B〉𝐹y) = z |
28 | 22, 27 | nfim 1461 |
. . . . . . 7
⊢
Ⅎx(∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅) → (〈A, B〉𝐹y) = z) |
29 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎy∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅) |
30 | | nfoprab2 5497 |
. . . . . . . . . . 11
⊢
Ⅎy{〈〈x, y〉,
z〉 ∣ ((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 𝑅))} |
31 | 8, 30 | nfcxfr 2172 |
. . . . . . . . . 10
⊢
Ⅎy𝐹 |
32 | 20, 31, 21 | nfov 5478 |
. . . . . . . . 9
⊢
Ⅎy(〈A, B〉𝐹〈𝐶, 𝐷〉) |
33 | 32 | nfeq1 2184 |
. . . . . . . 8
⊢
Ⅎy(〈A, B〉𝐹〈𝐶, 𝐷〉) = z |
34 | 29, 33 | nfim 1461 |
. . . . . . 7
⊢
Ⅎy(∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅) → (〈A, B〉𝐹〈𝐶, 𝐷〉) = z) |
35 | | eqeq1 2043 |
. . . . . . . . . . 11
⊢ (x = 〈A,
B〉 → (x = 〈w,
v〉 ↔ 〈A, B〉 =
〈w, v〉)) |
36 | 35 | anbi1d 438 |
. . . . . . . . . 10
⊢ (x = 〈A,
B〉 → ((x = 〈w,
v〉 ∧
y = 〈u, f〉)
↔ (〈A, B〉 = 〈w, v〉 ∧ y =
〈u, f〉))) |
37 | 36 | anbi1d 438 |
. . . . . . . . 9
⊢ (x = 〈A,
B〉 → (((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) ↔ ((〈A, B〉 =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 𝑅))) |
38 | 37 | 4exbidv 1747 |
. . . . . . . 8
⊢ (x = 〈A,
B〉 → (∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) ↔ ∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅))) |
39 | | oveq1 5462 |
. . . . . . . . 9
⊢ (x = 〈A,
B〉 → (x𝐹y) =
(〈A, B〉𝐹y)) |
40 | 39 | eqeq1d 2045 |
. . . . . . . 8
⊢ (x = 〈A,
B〉 → ((x𝐹y) =
z ↔ (〈A, B〉𝐹y) = z)) |
41 | 38, 40 | imbi12d 223 |
. . . . . . 7
⊢ (x = 〈A,
B〉 → ((∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) → (x𝐹y) =
z) ↔ (∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅) → (〈A, B〉𝐹y) = z))) |
42 | | eqeq1 2043 |
. . . . . . . . . . 11
⊢ (y = 〈𝐶, 𝐷〉 → (y = 〈u,
f〉 ↔ 〈𝐶, 𝐷〉 = 〈u, f〉)) |
43 | 42 | anbi2d 437 |
. . . . . . . . . 10
⊢ (y = 〈𝐶, 𝐷〉 → ((〈A, B〉 =
〈w, v〉 ∧ y = 〈u,
f〉) ↔ (〈A, B〉 =
〈w, v〉 ∧
〈𝐶, 𝐷〉 = 〈u, f〉))) |
44 | 43 | anbi1d 438 |
. . . . . . . . 9
⊢ (y = 〈𝐶, 𝐷〉 → (((〈A, B〉 =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 𝑅) ↔ ((〈A, B〉 =
〈w, v〉 ∧
〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅))) |
45 | 44 | 4exbidv 1747 |
. . . . . . . 8
⊢ (y = 〈𝐶, 𝐷〉 → (∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅) ↔ ∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅))) |
46 | | oveq2 5463 |
. . . . . . . . 9
⊢ (y = 〈𝐶, 𝐷〉 → (〈A, B〉𝐹y) = (〈A,
B〉𝐹〈𝐶, 𝐷〉)) |
47 | 46 | eqeq1d 2045 |
. . . . . . . 8
⊢ (y = 〈𝐶, 𝐷〉 → ((〈A, B〉𝐹y) = z ↔
(〈A, B〉𝐹〈𝐶, 𝐷〉) = z)) |
48 | 45, 47 | imbi12d 223 |
. . . . . . 7
⊢ (y = 〈𝐶, 𝐷〉 → ((∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅) → (〈A, B〉𝐹y) = z) ↔
(∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅) → (〈A, B〉𝐹〈𝐶, 𝐷〉) = z))) |
49 | | moeq 2710 |
. . . . . . . . . . . 12
⊢ ∃*z z = 𝑅 |
50 | 49 | mosubop 4349 |
. . . . . . . . . . 11
⊢ ∃*z∃u∃f(y = 〈u,
f〉 ∧
z = 𝑅) |
51 | 50 | mosubop 4349 |
. . . . . . . . . 10
⊢ ∃*z∃w∃v(x = 〈w,
v〉 ∧
∃u∃f(y = 〈u,
f〉 ∧
z = 𝑅)) |
52 | | anass 381 |
. . . . . . . . . . . . . 14
⊢
(((x = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 𝑅) ↔ (x = 〈w,
v〉 ∧
(y = 〈u, f〉 ∧ z = 𝑅))) |
53 | 52 | 2exbii 1494 |
. . . . . . . . . . . . 13
⊢ (∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) ↔ ∃u∃f(x = 〈w,
v〉 ∧
(y = 〈u, f〉 ∧ z = 𝑅))) |
54 | | 19.42vv 1785 |
. . . . . . . . . . . . 13
⊢ (∃u∃f(x = 〈w,
v〉 ∧
(y = 〈u, f〉 ∧ z = 𝑅)) ↔ (x = 〈w,
v〉 ∧
∃u∃f(y = 〈u,
f〉 ∧
z = 𝑅))) |
55 | 53, 54 | bitri 173 |
. . . . . . . . . . . 12
⊢ (∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) ↔ (x = 〈w,
v〉 ∧
∃u∃f(y = 〈u,
f〉 ∧
z = 𝑅))) |
56 | 55 | 2exbii 1494 |
. . . . . . . . . . 11
⊢ (∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) ↔ ∃w∃v(x = 〈w,
v〉 ∧
∃u∃f(y = 〈u,
f〉 ∧
z = 𝑅))) |
57 | 56 | mobii 1934 |
. . . . . . . . . 10
⊢ (∃*z∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) ↔ ∃*z∃w∃v(x = 〈w,
v〉 ∧
∃u∃f(y = 〈u,
f〉 ∧
z = 𝑅))) |
58 | 51, 57 | mpbir 134 |
. . . . . . . . 9
⊢ ∃*z∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) |
59 | 58 | a1i 9 |
. . . . . . . 8
⊢
((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) → ∃*z∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅)) |
60 | 59, 8 | ovidi 5561 |
. . . . . . 7
⊢
((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) → (∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
𝑅) → (x𝐹y) =
z)) |
61 | 19, 20, 21, 28, 34, 41, 48, 60 | vtocl2gaf 2614 |
. . . . . 6
⊢
((〈A, B〉 ∈ (𝐻 × 𝐻) ∧
〈𝐶, 𝐷〉 ∈
(𝐻 × 𝐻)) → (∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅) → (〈A, B〉𝐹〈𝐶, 𝐷〉) = z)) |
62 | 17, 18, 61 | syl2an 273 |
. . . . 5
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃w∃v∃u∃f((〈A,
B〉 = 〈w, v〉 ∧ 〈𝐶, 𝐷〉 = 〈u, f〉)
∧ z =
𝑅) → (〈A, B〉𝐹〈𝐶, 𝐷〉) = z)) |
63 | 16, 62 | sylbird 159 |
. . . 4
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (z = 𝑆 → (〈A, B〉𝐹〈𝐶, 𝐷〉) = z)) |
64 | | eqeq2 2046 |
. . . 4
⊢ (z = 𝑆 → ((〈A, B〉𝐹〈𝐶, 𝐷〉) = z ↔ (〈A, B〉𝐹〈𝐶, 𝐷〉) = 𝑆)) |
65 | 63, 64 | mpbidi 140 |
. . 3
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (z = 𝑆 → (〈A, B〉𝐹〈𝐶, 𝐷〉) = 𝑆)) |
66 | 6, 13, 65 | exlimd 1485 |
. 2
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃z z = 𝑆 → (〈A, B〉𝐹〈𝐶, 𝐷〉) = 𝑆)) |
67 | 5, 66 | mpd 13 |
1
⊢
(((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈A, B〉𝐹〈𝐶, 𝐷〉) = 𝑆) |