Step | Hyp | Ref
| Expression |
1 | | enq0er 7397 |
. . . . . . . . . . . . . 14
⊢
~Q0 Er (ω ×
N) |
2 | 1 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ ~Q0 Er (ω ×
N)) |
3 | | nnnq0lem1 7408 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ ((((𝑤 ∈ ω
∧ 𝑣 ∈
N) ∧ (𝑠
∈ ω ∧ 𝑓
∈ N)) ∧ ((𝑢 ∈ ω ∧ 𝑡 ∈ N) ∧ (𝑔 ∈ ω ∧ ℎ ∈ N))) ∧
((𝑤 ·o
𝑓) = (𝑣 ·o 𝑠) ∧ (𝑢 ·o ℎ) = (𝑡 ·o 𝑔)))) |
4 | | mulcmpblnq0 7406 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧
(𝑠 ∈ ω ∧
𝑓 ∈ N))
∧ ((𝑢 ∈ ω
∧ 𝑡 ∈
N) ∧ (𝑔
∈ ω ∧ ℎ
∈ N))) → (((𝑤 ·o 𝑓) = (𝑣 ·o 𝑠) ∧ (𝑢 ·o ℎ) = (𝑡 ·o 𝑔)) → 〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉 ~Q0
〈(𝑠
·o 𝑔),
(𝑓 ·o
ℎ)〉)) |
5 | 4 | imp 123 |
. . . . . . . . . . . . . 14
⊢
(((((𝑤 ∈
ω ∧ 𝑣 ∈
N) ∧ (𝑠
∈ ω ∧ 𝑓
∈ N)) ∧ ((𝑢 ∈ ω ∧ 𝑡 ∈ N) ∧ (𝑔 ∈ ω ∧ ℎ ∈ N))) ∧
((𝑤 ·o
𝑓) = (𝑣 ·o 𝑠) ∧ (𝑢 ·o ℎ) = (𝑡 ·o 𝑔))) → 〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉 ~Q0
〈(𝑠
·o 𝑔),
(𝑓 ·o
ℎ)〉) |
6 | 3, 5 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ 〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉
~Q0 〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉) |
7 | 2, 6 | erthi 6559 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ [〈(𝑤
·o 𝑢),
(𝑣 ·o
𝑡)〉]
~Q0 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0
) |
8 | | simprlr 533 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ 𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
) |
9 | | simprrr 535 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ 𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0
) |
10 | 7, 8, 9 | 3eqtr4d 2213 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 )))
→ 𝑧 = 𝑞) |
11 | 10 | expr 373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ (((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ) →
𝑧 = 𝑞)) |
12 | 11 | exlimdvv 1890 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ (∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ) →
𝑧 = 𝑞)) |
13 | 12 | exlimdvv 1890 |
. . . . . . . 8
⊢ (((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ) →
𝑧 = 𝑞)) |
14 | 13 | ex 114 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
→ (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ) →
𝑧 = 𝑞))) |
15 | 14 | exlimdvv 1890 |
. . . . . 6
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → (∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
→ (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ) →
𝑧 = 𝑞))) |
16 | 15 | exlimdvv 1890 |
. . . . 5
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
→ (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ) →
𝑧 = 𝑞))) |
17 | 16 | impd 252 |
. . . 4
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → ((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ))
→ 𝑧 = 𝑞)) |
18 | 17 | alrimivv 1868 |
. . 3
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ))
→ 𝑧 = 𝑞)) |
19 | | opeq12 3767 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈𝑤, 𝑣〉 = 〈𝑠, 𝑓〉) |
20 | 19 | eceq1d 6549 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈𝑤, 𝑣〉] ~Q0 =
[〈𝑠, 𝑓〉]
~Q0 ) |
21 | 20 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝐴 = [〈𝑤, 𝑣〉] ~Q0 ↔
𝐴 = [〈𝑠, 𝑓〉] ~Q0
)) |
22 | 21 | anbi1d 462 |
. . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → ((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0
))) |
23 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑤 = 𝑠) |
24 | 23 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑤 ·o 𝑢) = (𝑠 ·o 𝑢)) |
25 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑣 = 𝑓) |
26 | 25 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑣 ·o 𝑡) = (𝑓 ·o 𝑡)) |
27 | 24, 26 | opeq12d 3773 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉 = 〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉) |
28 | 27 | eceq1d 6549 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 =
[〈(𝑠
·o 𝑢),
(𝑓 ·o
𝑡)〉]
~Q0 ) |
29 | 28 | eqeq2d 2182 |
. . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ↔
𝑞 = [〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉] ~Q0
)) |
30 | 22, 29 | anbi12d 470 |
. . . . . . 7
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉] ~Q0
))) |
31 | | opeq12 3767 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈𝑢, 𝑡〉 = 〈𝑔, ℎ〉) |
32 | 31 | eceq1d 6549 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈𝑢, 𝑡〉] ~Q0 =
[〈𝑔, ℎ〉]
~Q0 ) |
33 | 32 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝐵 = [〈𝑢, 𝑡〉] ~Q0 ↔
𝐵 = [〈𝑔, ℎ〉] ~Q0
)) |
34 | 33 | anbi2d 461 |
. . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0
))) |
35 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑢 = 𝑔) |
36 | 35 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑠 ·o 𝑢) = (𝑠 ·o 𝑔)) |
37 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑡 = ℎ) |
38 | 37 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑓 ·o 𝑡) = (𝑓 ·o ℎ)) |
39 | 36, 38 | opeq12d 3773 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉 = 〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉) |
40 | 39 | eceq1d 6549 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉] ~Q0 =
[〈(𝑠
·o 𝑔),
(𝑓 ·o
ℎ)〉]
~Q0 ) |
41 | 40 | eqeq2d 2182 |
. . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑞 = [〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉] ~Q0 ↔
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0
)) |
42 | 34, 41 | anbi12d 470 |
. . . . . . 7
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑢), (𝑓 ·o 𝑡)〉] ~Q0 )
↔ ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0
))) |
43 | 30, 42 | cbvex4v 1923 |
. . . . . 6
⊢
(∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0
)) |
44 | 43 | anbi2i 454 |
. . . . 5
⊢
((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
↔ (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0
))) |
45 | 44 | imbi1i 237 |
. . . 4
⊢
(((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ 𝑧 = 𝑞) ↔ ((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ))
→ 𝑧 = 𝑞)) |
46 | 45 | 2albii 1464 |
. . 3
⊢
(∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ 𝑧 = 𝑞) ↔ ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~Q0 ∧
𝐵 = [〈𝑔, ℎ〉] ~Q0 ) ∧
𝑞 = [〈(𝑠 ·o 𝑔), (𝑓 ·o ℎ)〉] ~Q0 ))
→ 𝑧 = 𝑞)) |
47 | 18, 46 | sylibr 133 |
. 2
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ 𝑧 = 𝑞)) |
48 | | eqeq1 2177 |
. . . . 5
⊢ (𝑧 = 𝑞 → (𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ↔
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
)) |
49 | 48 | anbi2d 461 |
. . . 4
⊢ (𝑧 = 𝑞 → (((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ ((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
))) |
50 | 49 | 4exbidv 1863 |
. . 3
⊢ (𝑧 = 𝑞 → (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
))) |
51 | 50 | mo4 2080 |
. 2
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 )
↔ ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑞 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0 ))
→ 𝑧 = 𝑞)) |
52 | 47, 51 | sylibr 133 |
1
⊢ ((𝐴 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝐵 ∈ ((ω ×
N) / ~Q0 )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝐵 = [〈𝑢, 𝑡〉] ~Q0 ) ∧
𝑧 = [〈(𝑤 ·o 𝑢), (𝑣 ·o 𝑡)〉] ~Q0
)) |