Proof of Theorem th3q
Step | Hyp | Ref
| Expression |
1 | | opelxpi 4319 |
. . . 4
⊢
((A ∈ 𝑆 ∧ B ∈ 𝑆) → 〈A, B〉 ∈ (𝑆 × 𝑆)) |
2 | | th3q.1 |
. . . . 5
⊢ ∼ ∈ V |
3 | 2 | ecelqsi 6096 |
. . . 4
⊢
(〈A, B〉 ∈ (𝑆 × 𝑆) → [〈A, B〉]
∼
∈ ((𝑆 × 𝑆) / ∼ )) |
4 | 1, 3 | syl 14 |
. . 3
⊢
((A ∈ 𝑆 ∧ B ∈ 𝑆) → [〈A, B〉]
∼
∈ ((𝑆 × 𝑆) / ∼ )) |
5 | | opelxpi 4319 |
. . . 4
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 〈𝐶, 𝐷〉 ∈
(𝑆 × 𝑆)) |
6 | 2 | ecelqsi 6096 |
. . . 4
⊢
(〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆) → [〈𝐶, 𝐷〉] ∼ ∈ ((𝑆 × 𝑆) / ∼ )) |
7 | 5, 6 | syl 14 |
. . 3
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → [〈𝐶, 𝐷〉] ∼ ∈ ((𝑆 × 𝑆) / ∼ )) |
8 | 4, 7 | anim12i 321 |
. 2
⊢
(((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈A, B〉]
∼
∈ ((𝑆 × 𝑆) / ∼ ) ∧ [〈𝐶, 𝐷〉] ∼ ∈ ((𝑆 × 𝑆) / ∼
))) |
9 | | eqid 2037 |
. . . 4
⊢
[〈A, B〉] ∼ = [〈A, B〉]
∼ |
10 | | eqid 2037 |
. . . 4
⊢
[〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ |
11 | 9, 10 | pm3.2i 257 |
. . 3
⊢
([〈A, B〉] ∼ = [〈A, B〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) |
12 | | eqid 2037 |
. . 3
⊢
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ |
13 | | opeq12 3542 |
. . . . . 6
⊢
((w = A ∧ v = B) →
〈w, v〉 = 〈A, B〉) |
14 | | eceq1 6077 |
. . . . . . . . 9
⊢
(〈w, v〉 = 〈A, B〉
→ [〈w, v〉] ∼ = [〈A, B〉]
∼
) |
15 | 14 | eqeq2d 2048 |
. . . . . . . 8
⊢
(〈w, v〉 = 〈A, B〉
→ ([〈A, B〉] ∼ = [〈w, v〉]
∼
↔ [〈A, B〉] ∼ = [〈A, B〉]
∼
)) |
16 | 15 | anbi1d 438 |
. . . . . . 7
⊢
(〈w, v〉 = 〈A, B〉
→ (([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ↔
([〈A, B〉] ∼ = [〈A, B〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼
))) |
17 | | oveq1 5462 |
. . . . . . . . 9
⊢
(〈w, v〉 = 〈A, B〉
→ (〈w, v〉 + 〈𝐶, 𝐷〉) = (〈A, B〉 + 〈𝐶, 𝐷〉)) |
18 | 17 | eceq1d 6078 |
. . . . . . . 8
⊢
(〈w, v〉 = 〈A, B〉
→ [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) |
19 | 18 | eqeq2d 2048 |
. . . . . . 7
⊢
(〈w, v〉 = 〈A, B〉
→ ([(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ ↔
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ )) |
20 | 16, 19 | anbi12d 442 |
. . . . . 6
⊢
(〈w, v〉 = 〈A, B〉
→ ((([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ ) ↔
(([〈A, B〉] ∼ = [〈A, B〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼
))) |
21 | 13, 20 | syl 14 |
. . . . 5
⊢
((w = A ∧ v = B) →
((([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ ) ↔
(([〈A, B〉] ∼ = [〈A, B〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼
))) |
22 | 21 | spc2egv 2636 |
. . . 4
⊢
((A ∈ 𝑆 ∧ B ∈ 𝑆) → ((([〈A, B〉]
∼
= [〈A, B〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) → ∃w∃v(([〈A,
B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼
))) |
23 | | opeq12 3542 |
. . . . . . 7
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → 〈u, 𝑡〉 = 〈𝐶, 𝐷〉) |
24 | | eceq1 6077 |
. . . . . . . . . 10
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → [〈u, 𝑡〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) |
25 | 24 | eqeq2d 2048 |
. . . . . . . . 9
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → ([〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ↔ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ )) |
26 | 25 | anbi2d 437 |
. . . . . . . 8
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → (([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ↔
([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼
))) |
27 | | oveq2 5463 |
. . . . . . . . . 10
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → (〈w, v〉 +
〈u, 𝑡〉) = (〈w, v〉 + 〈𝐶, 𝐷〉)) |
28 | 27 | eceq1d 6078 |
. . . . . . . . 9
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → [(〈w, v〉 +
〈u, 𝑡〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ ) |
29 | 28 | eqeq2d 2048 |
. . . . . . . 8
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → ([(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ ↔
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ )) |
30 | 26, 29 | anbi12d 442 |
. . . . . . 7
⊢
(〈u, 𝑡〉 = 〈𝐶, 𝐷〉 → ((([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ ) ↔
(([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼
))) |
31 | 23, 30 | syl 14 |
. . . . . 6
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → ((([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ ) ↔
(([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼
))) |
32 | 31 | spc2egv 2636 |
. . . . 5
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → ((([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ ) → ∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼
))) |
33 | 32 | 2eximdv 1759 |
. . . 4
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (∃w∃v(([〈A,
B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 + 〈𝐶, 𝐷〉)] ∼ ) → ∃w∃v∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼
))) |
34 | 22, 33 | sylan9 389 |
. . 3
⊢
(((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ((([〈A, B〉]
∼
= [〈A, B〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) → ∃w∃v∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼
))) |
35 | 11, 12, 34 | mp2ani 408 |
. 2
⊢
(((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ∃w∃v∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ )) |
36 | | ecexg 6046 |
. . . 4
⊢ ( ∼ ∈ V → [(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ∈ V) |
37 | 2, 36 | ax-mp 7 |
. . 3
⊢
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ∈ V |
38 | | eqeq1 2043 |
. . . . . . . 8
⊢ (x = [〈A,
B〉] ∼ → (x = [〈w,
v〉] ∼ ↔
[〈A, B〉] ∼ = [〈w, v〉]
∼
)) |
39 | | eqeq1 2043 |
. . . . . . . 8
⊢ (y = [〈𝐶, 𝐷〉] ∼ → (y = [〈u,
𝑡〉] ∼ ↔ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ )) |
40 | 38, 39 | bi2anan9 538 |
. . . . . . 7
⊢
((x = [〈A, B〉]
∼
∧ y =
[〈𝐶, 𝐷〉] ∼ ) → ((x = [〈w,
v〉] ∼ ∧ y =
[〈u, 𝑡〉] ∼ ) ↔
([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼
))) |
41 | | eqeq1 2043 |
. . . . . . 7
⊢ (z = [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ → (z = [(〈w,
v〉 + 〈u, 𝑡〉)] ∼ ↔
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ )) |
42 | 40, 41 | bi2anan9 538 |
. . . . . 6
⊢
(((x = [〈A, B〉]
∼
∧ y =
[〈𝐶, 𝐷〉] ∼ ) ∧ z =
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) →
(((x = [〈w, v〉]
∼
∧ y =
[〈u, 𝑡〉] ∼ ) ∧ z =
[(〈w, v〉 + 〈u, 𝑡〉)] ∼ ) ↔
(([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼
))) |
43 | 42 | 3impa 1098 |
. . . . 5
⊢
((x = [〈A, B〉]
∼
∧ y =
[〈𝐶, 𝐷〉] ∼ ∧ z =
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) →
(((x = [〈w, v〉]
∼
∧ y =
[〈u, 𝑡〉] ∼ ) ∧ z =
[(〈w, v〉 + 〈u, 𝑡〉)] ∼ ) ↔
(([〈A, B〉] ∼ = [〈w, v〉]
∼
∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼
))) |
44 | 43 | 4exbidv 1747 |
. . . 4
⊢
((x = [〈A, B〉]
∼
∧ y =
[〈𝐶, 𝐷〉] ∼ ∧ z =
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) → (∃w∃v∃u∃𝑡((x =
[〈w, v〉] ∼ ∧ y =
[〈u, 𝑡〉] ∼ ) ∧ z =
[(〈w, v〉 + 〈u, 𝑡〉)] ∼ ) ↔ ∃w∃v∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼
))) |
45 | | th3q.2 |
. . . . 5
⊢ ∼ Er
(𝑆 × 𝑆) |
46 | | th3q.4 |
. . . . 5
⊢
((((w ∈ 𝑆 ∧ v ∈ 𝑆) ∧ (u ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧
((𝑠 ∈ 𝑆 ∧ f ∈ 𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈
𝑆))) →
((〈w, v〉 ∼ 〈u, 𝑡〉 ∧
〈𝑠, f〉 ∼ 〈g, ℎ〉) → (〈w, v〉 + 〈𝑠, f〉) ∼ (〈u, 𝑡〉 + 〈g, ℎ〉))) |
47 | 2, 45, 46 | th3qlem2 6145 |
. . . 4
⊢
((x ∈ ((𝑆 × 𝑆) / ∼ ) ∧ y ∈ ((𝑆 × 𝑆) / ∼ )) → ∃*z∃w∃v∃u∃𝑡((x =
[〈w, v〉] ∼ ∧ y =
[〈u, 𝑡〉] ∼ ) ∧ z =
[(〈w, v〉 + 〈u, 𝑡〉)] ∼ )) |
48 | | th3q.5 |
. . . 4
⊢ 𝐺 = {〈〈x, y〉,
z〉 ∣ ((x ∈ ((𝑆 × 𝑆) / ∼ ) ∧ y ∈ ((𝑆 × 𝑆) / ∼ )) ∧ ∃w∃v∃u∃𝑡((x =
[〈w, v〉] ∼ ∧ y =
[〈u, 𝑡〉] ∼ ) ∧ z =
[(〈w, v〉 + 〈u, 𝑡〉)] ∼
))} |
49 | 44, 47, 48 | ovig 5564 |
. . 3
⊢
(([〈A, B〉] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [〈𝐶, 𝐷〉] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ ∈ V) → (∃w∃v∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ ) →
([〈A, B〉] ∼ 𝐺[〈𝐶, 𝐷〉] ∼ ) =
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ )) |
50 | 37, 49 | mp3an3 1220 |
. 2
⊢
(([〈A, B〉] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [〈𝐶, 𝐷〉] ∼ ∈ ((𝑆 × 𝑆) / ∼ )) → (∃w∃v∃u∃𝑡(([〈A, B〉]
∼
= [〈w, v〉] ∼ ∧ [〈𝐶, 𝐷〉] ∼ = [〈u, 𝑡〉] ∼ ) ∧ [(〈A,
B〉 + 〈𝐶, 𝐷〉)] ∼ = [(〈w, v〉 +
〈u, 𝑡〉)] ∼ ) →
([〈A, B〉] ∼ 𝐺[〈𝐶, 𝐷〉] ∼ ) =
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ )) |
51 | 8, 35, 50 | sylc 56 |
1
⊢
(((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈A, B〉]
∼
𝐺[〈𝐶, 𝐷〉] ∼ ) =
[(〈A, B〉 + 〈𝐶, 𝐷〉)] ∼ ) |