Step | Hyp | Ref
| Expression |
1 | | opelxpi 4643 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) →
〈𝐴, 𝐵〉 ∈ (ω ×
N)) |
2 | | enq0ex 7401 |
. . . . 5
⊢
~Q0 ∈ V |
3 | 2 | ecelqsi 6567 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ (ω ×
N) → [〈𝐴, 𝐵〉] ~Q0 ∈
((ω × N) / ~Q0
)) |
4 | 1, 3 | syl 14 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) →
[〈𝐴, 𝐵〉] ~Q0 ∈
((ω × N) / ~Q0
)) |
5 | | opelxpi 4643 |
. . . 4
⊢ ((𝐶 ∈ ω ∧ 𝐷 ∈ N) →
〈𝐶, 𝐷〉 ∈ (ω ×
N)) |
6 | 2 | ecelqsi 6567 |
. . . 4
⊢
(〈𝐶, 𝐷〉 ∈ (ω ×
N) → [〈𝐶, 𝐷〉] ~Q0 ∈
((ω × N) / ~Q0
)) |
7 | 5, 6 | syl 14 |
. . 3
⊢ ((𝐶 ∈ ω ∧ 𝐷 ∈ N) →
[〈𝐶, 𝐷〉] ~Q0 ∈
((ω × N) / ~Q0
)) |
8 | 4, 7 | anim12i 336 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ ω ∧
𝐷 ∈ N))
→ ([〈𝐴, 𝐵〉]
~Q0 ∈ ((ω × N) /
~Q0 ) ∧ [〈𝐶, 𝐷〉] ~Q0 ∈
((ω × N) / ~Q0
))) |
9 | | eqid 2170 |
. . . 4
⊢
[〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉]
~Q0 |
10 | | eqid 2170 |
. . . 4
⊢
[〈𝐶, 𝐷〉]
~Q0 = [〈𝐶, 𝐷〉]
~Q0 |
11 | 9, 10 | pm3.2i 270 |
. . 3
⊢
([〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0
) |
12 | | eqid 2170 |
. . 3
⊢
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉]
~Q0 |
13 | | opeq12 3767 |
. . . . . 6
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉) |
14 | | eceq1 6548 |
. . . . . . . . 9
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → [〈𝑤, 𝑣〉] ~Q0 =
[〈𝐴, 𝐵〉] ~Q0
) |
15 | 14 | eqeq2d 2182 |
. . . . . . . 8
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → ([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ↔ [〈𝐴, 𝐵〉] ~Q0 =
[〈𝐴, 𝐵〉] ~Q0
)) |
16 | 15 | anbi1d 462 |
. . . . . . 7
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → (([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 )
↔ ([〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0
))) |
17 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
18 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑣 ∈ V |
19 | 17, 18 | opth 4222 |
. . . . . . . . . 10
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 ↔ (𝑤 = 𝐴 ∧ 𝑣 = 𝐵)) |
20 | | oveq1 5860 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝐴 → (𝑤 ·o 𝐶) = (𝐴 ·o 𝐶)) |
21 | 20 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑤 ·o 𝐶) = (𝐴 ·o 𝐶)) |
22 | | oveq1 5860 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → (𝑣 ·o 𝐷) = (𝐵 ·o 𝐷)) |
23 | 22 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑣 ·o 𝐷) = (𝐵 ·o 𝐷)) |
24 | 21, 23 | opeq12d 3773 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉 = 〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉) |
25 | 19, 24 | sylbi 120 |
. . . . . . . . 9
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → 〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉 = 〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉) |
26 | 25 | eceq1d 6549 |
. . . . . . . 8
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0 =
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 ) |
27 | 26 | eqeq2d 2182 |
. . . . . . 7
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → ([〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝐶),
(𝑣 ·o
𝐷)〉]
~Q0 ↔ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 )) |
28 | 16, 27 | anbi12d 470 |
. . . . . 6
⊢
(〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉 → ((([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0 )
↔ (([〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0
))) |
29 | 13, 28 | syl 14 |
. . . . 5
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0 )
↔ (([〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0
))) |
30 | 29 | spc2egv 2820 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) →
((([〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 )
→ ∃𝑤∃𝑣(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0
))) |
31 | | opeq12 3767 |
. . . . . . 7
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉) |
32 | | eceq1 6548 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → [〈𝑢, 𝑡〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0
) |
33 | 32 | eqeq2d 2182 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → ([〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ↔ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0
)) |
34 | 33 | anbi2d 461 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → (([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ↔ ([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0
))) |
35 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
36 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
37 | 35, 36 | opth 4222 |
. . . . . . . . . . 11
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 ↔ (𝑢 = 𝐶 ∧ 𝑡 = 𝐷)) |
38 | | oveq2 5861 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐶 → (𝑤 ·o 𝑢) = (𝑤 ·o 𝐶)) |
39 | 38 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑤 ·o 𝑢) = (𝑤 ·o 𝐶)) |
40 | | oveq2 5861 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝐷 → (𝑣 ·o 𝑡) = (𝑣 ·o 𝐷)) |
41 | 40 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑣 ·o 𝑡) = (𝑣 ·o 𝐷)) |
42 | 39, 41 | opeq12d 3773 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉 = 〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉) |
43 | 37, 42 | sylbi 120 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → 〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉 = 〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉) |
44 | 43 | eceq1d 6549 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 =
[〈(𝑤
·o 𝐶),
(𝑣 ·o
𝐷)〉]
~Q0 ) |
45 | 44 | eqeq2d 2182 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → ([〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ↔ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝐶),
(𝑣 ·o
𝐷)〉]
~Q0 )) |
46 | 34, 45 | anbi12d 470 |
. . . . . . 7
⊢
(〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉 → ((([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ) ↔ (([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0
))) |
47 | 31, 46 | syl 14 |
. . . . . 6
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ((([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ) ↔ (([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0
))) |
48 | 47 | spc2egv 2820 |
. . . . 5
⊢ ((𝐶 ∈ ω ∧ 𝐷 ∈ N) →
((([〈𝐴, 𝐵〉]
~Q0 = [〈𝑤, 𝑣〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0 )
→ ∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ))) |
49 | 48 | 2eximdv 1875 |
. . . 4
⊢ ((𝐶 ∈ ω ∧ 𝐷 ∈ N) →
(∃𝑤∃𝑣(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝐶), (𝑣 ·o 𝐷)〉] ~Q0 )
→ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ))) |
50 | 30, 49 | sylan9 407 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ ω ∧
𝐷 ∈ N))
→ ((([〈𝐴, 𝐵〉]
~Q0 = [〈𝐴, 𝐵〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝐶, 𝐷〉] ~Q0 ) ∧
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 )
→ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ))) |
51 | 11, 12, 50 | mp2ani 430 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ ω ∧
𝐷 ∈ N))
→ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 )) |
52 | | ecexg 6517 |
. . . 4
⊢ (
~Q0 ∈ V → [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 ∈
V) |
53 | 2, 52 | ax-mp 5 |
. . 3
⊢
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 ∈ V |
54 | | eqeq1 2177 |
. . . . . . . 8
⊢ (𝑥 = [〈𝐴, 𝐵〉] ~Q0 →
(𝑥 = [〈𝑤, 𝑣〉] ~Q0 ↔
[〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 )) |
55 | | eqeq1 2177 |
. . . . . . . 8
⊢ (𝑦 = [〈𝐶, 𝐷〉] ~Q0 →
(𝑦 = [〈𝑢, 𝑡〉] ~Q0 ↔
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 )) |
56 | 54, 55 | bi2anan9 601 |
. . . . . . 7
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~Q0 ∧
𝑦 = [〈𝐶, 𝐷〉] ~Q0 )
→ ((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑡〉] ~Q0 ) ↔
([〈𝐴, 𝐵〉]
~Q0 = [〈𝑤, 𝑣〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ))) |
57 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑧 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 →
(𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ↔
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
)) |
58 | 56, 57 | bi2anan9 601 |
. . . . . 6
⊢ (((𝑥 = [〈𝐴, 𝐵〉] ~Q0 ∧
𝑦 = [〈𝐶, 𝐷〉] ~Q0 ) ∧
𝑧 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 )
→ (((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ (([〈𝐴, 𝐵〉]
~Q0 = [〈𝑤, 𝑣〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ))) |
59 | 58 | 3impa 1189 |
. . . . 5
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~Q0 ∧
𝑦 = [〈𝐶, 𝐷〉] ~Q0 ∧
𝑧 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 )
→ (((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ (([〈𝐴, 𝐵〉]
~Q0 = [〈𝑤, 𝑣〉] ~Q0 ∧
[〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ))) |
60 | 59 | 4exbidv 1863 |
. . . 4
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~Q0 ∧
𝑦 = [〈𝐶, 𝐷〉] ~Q0 ∧
𝑧 = [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 )
→ (∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ))) |
61 | | mulnq0mo 7410 |
. . . 4
⊢ ((𝑥 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝑦 ∈ ((ω ×
N) / ~Q0 )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
)) |
62 | | dfmq0qs 7391 |
. . . 4
⊢
·Q0 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((ω × N)
/ ~Q0 ) ∧ 𝑦 ∈ ((ω × N)
/ ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
))} |
63 | 60, 61, 62 | ovig 5974 |
. . 3
⊢
(([〈𝐴, 𝐵〉]
~Q0 ∈ ((ω × N) /
~Q0 ) ∧ [〈𝐶, 𝐷〉] ~Q0 ∈
((ω × N) / ~Q0 )
∧ [〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 ∈ V) → (∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ) → ([〈𝐴, 𝐵〉] ~Q0
·Q0 [〈𝐶, 𝐷〉] ~Q0 ) =
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 )) |
64 | 53, 63 | mp3an3 1321 |
. 2
⊢
(([〈𝐴, 𝐵〉]
~Q0 ∈ ((ω × N) /
~Q0 ) ∧ [〈𝐶, 𝐷〉] ~Q0 ∈
((ω × N) / ~Q0 ))
→ (∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~Q0 =
[〈𝑤, 𝑣〉]
~Q0 ∧ [〈𝐶, 𝐷〉] ~Q0 =
[〈𝑢, 𝑡〉]
~Q0 ) ∧ [〈(𝐴 ·o 𝐶), (𝐵 ·o 𝐷)〉] ~Q0 =
[〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 ) → ([〈𝐴, 𝐵〉] ~Q0
·Q0 [〈𝐶, 𝐷〉] ~Q0 ) =
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 )) |
65 | 8, 51, 64 | sylc 62 |
1
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ ω ∧
𝐷 ∈ N))
→ ([〈𝐴, 𝐵〉]
~Q0 ·Q0 [〈𝐶, 𝐷〉] ~Q0 ) =
[〈(𝐴
·o 𝐶),
(𝐵 ·o
𝐷)〉]
~Q0 ) |