Proof of Theorem oviec
Step | Hyp | Ref
| Expression |
1 | | oviec.4 |
. . 3
⊢ ∼ ∈
V |
2 | | oviec.5 |
. . 3
⊢ ∼ Er
(𝑆 × 𝑆) |
3 | | oviec.16 |
. . . 4
⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((𝜓 ∧ 𝜒) → 𝐾 ∼ 𝐿)) |
4 | | oviec.8 |
. . . . . 6
⊢ (((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) ∧ (𝑣 = 𝑐 ∧ 𝑢 = 𝑑)) → (𝜑 ↔ 𝜓)) |
5 | | oviec.7 |
. . . . . 6
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑))} |
6 | 4, 5 | opbrop 4668 |
. . . . 5
⊢ (((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → (〈𝑎, 𝑏〉 ∼ 〈𝑐, 𝑑〉 ↔ 𝜓)) |
7 | | oviec.9 |
. . . . . 6
⊢ (((𝑧 = 𝑔 ∧ 𝑤 = ℎ) ∧ (𝑣 = 𝑡 ∧ 𝑢 = 𝑠)) → (𝜑 ↔ 𝜒)) |
8 | 7, 5 | opbrop 4668 |
. . . . 5
⊢ (((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → (〈𝑔, ℎ〉 ∼ 〈𝑡, 𝑠〉 ↔ 𝜒)) |
9 | 6, 8 | bi2anan9 596 |
. . . 4
⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((〈𝑎, 𝑏〉 ∼ 〈𝑐, 𝑑〉 ∧ 〈𝑔, ℎ〉 ∼ 〈𝑡, 𝑠〉) ↔ (𝜓 ∧ 𝜒))) |
10 | | oviec.2 |
. . . . . . 7
⊢ (((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → 𝐾 ∈ (𝑆 × 𝑆)) |
11 | | oviec.11 |
. . . . . . 7
⊢ (((𝑤 = 𝑎 ∧ 𝑣 = 𝑏) ∧ (𝑢 = 𝑔 ∧ 𝑓 = ℎ)) → 𝐽 = 𝐾) |
12 | | oviec.10 |
. . . . . . 7
⊢ + =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝐽))} |
13 | 10, 11, 12 | ovi3 5960 |
. . . . . 6
⊢ (((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → (〈𝑎, 𝑏〉 + 〈𝑔, ℎ〉) = 𝐾) |
14 | | oviec.3 |
. . . . . . 7
⊢ (((𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → 𝐿 ∈ (𝑆 × 𝑆)) |
15 | | oviec.12 |
. . . . . . 7
⊢ (((𝑤 = 𝑐 ∧ 𝑣 = 𝑑) ∧ (𝑢 = 𝑡 ∧ 𝑓 = 𝑠)) → 𝐽 = 𝐿) |
16 | 14, 15, 12 | ovi3 5960 |
. . . . . 6
⊢ (((𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → (〈𝑐, 𝑑〉 + 〈𝑡, 𝑠〉) = 𝐿) |
17 | 13, 16 | breqan12d 3983 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) ∧ ((𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((〈𝑎, 𝑏〉 + 〈𝑔, ℎ〉) ∼ (〈𝑐, 𝑑〉 + 〈𝑡, 𝑠〉) ↔ 𝐾 ∼ 𝐿)) |
18 | 17 | an4s 578 |
. . . 4
⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((〈𝑎, 𝑏〉 + 〈𝑔, ℎ〉) ∼ (〈𝑐, 𝑑〉 + 〈𝑡, 𝑠〉) ↔ 𝐾 ∼ 𝐿)) |
19 | 3, 9, 18 | 3imtr4d 202 |
. . 3
⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((〈𝑎, 𝑏〉 ∼ 〈𝑐, 𝑑〉 ∧ 〈𝑔, ℎ〉 ∼ 〈𝑡, 𝑠〉) → (〈𝑎, 𝑏〉 + 〈𝑔, ℎ〉) ∼ (〈𝑐, 𝑑〉 + 〈𝑡, 𝑠〉))) |
20 | | oviec.14 |
. . . 4
⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼
))} |
21 | | oviec.15 |
. . . . . . . 8
⊢ 𝑄 = ((𝑆 × 𝑆) / ∼ ) |
22 | 21 | eleq2i 2224 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑄 ↔ 𝑥 ∈ ((𝑆 × 𝑆) / ∼ )) |
23 | 21 | eleq2i 2224 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑄 ↔ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) |
24 | 22, 23 | anbi12i 456 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ (𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼
))) |
25 | 24 | anbi1i 454 |
. . . . 5
⊢ (((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼ )) ↔ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧
∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼
))) |
26 | 25 | oprabbii 5879 |
. . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼ ))} =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧
∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼
))} |
27 | 20, 26 | eqtri 2178 |
. . 3
⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧
∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼
))} |
28 | 1, 2, 19, 27 | th3q 6588 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈𝐴, 𝐵〉] ∼ ⨣ [〈𝐶, 𝐷〉] ∼ ) = [(〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉)] ∼ ) |
29 | | oviec.1 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐻 ∈ (𝑆 × 𝑆)) |
30 | | oviec.13 |
. . . 4
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝐽 = 𝐻) |
31 | 29, 30, 12 | ovi3 5960 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉) = 𝐻) |
32 | 31 | eceq1d 6519 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → [(〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉)] ∼ = [𝐻] ∼ ) |
33 | 28, 32 | eqtrd 2190 |
1
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈𝐴, 𝐵〉] ∼ ⨣ [〈𝐶, 𝐷〉] ∼ ) = [𝐻] ∼ ) |