Step | Hyp | Ref
| Expression |
1 | | elqsi 8542 |
. . . . . . . 8
⊢ (𝑋 ∈ (𝐴 / 𝑅) → ∃𝑝 ∈ 𝐴 𝑋 = [𝑝]𝑅) |
2 | | eropr.1 |
. . . . . . . 8
⊢ 𝐽 = (𝐴 / 𝑅) |
3 | 1, 2 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐽 → ∃𝑝 ∈ 𝐴 𝑋 = [𝑝]𝑅) |
4 | | elqsi 8542 |
. . . . . . . 8
⊢ (𝑌 ∈ (𝐵 / 𝑆) → ∃𝑞 ∈ 𝐵 𝑌 = [𝑞]𝑆) |
5 | | eropr.2 |
. . . . . . . 8
⊢ 𝐾 = (𝐵 / 𝑆) |
6 | 4, 5 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐾 → ∃𝑞 ∈ 𝐵 𝑌 = [𝑞]𝑆) |
7 | 3, 6 | anim12i 613 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾) → (∃𝑝 ∈ 𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞 ∈ 𝐵 𝑌 = [𝑞]𝑆)) |
8 | 7 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → (∃𝑝 ∈ 𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞 ∈ 𝐵 𝑌 = [𝑞]𝑆)) |
9 | | reeanv 3295 |
. . . . 5
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 (𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ (∃𝑝 ∈ 𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞 ∈ 𝐵 𝑌 = [𝑞]𝑆)) |
10 | 8, 9 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 (𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆)) |
11 | | eropr.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝑍) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → 𝑇 ∈ 𝑍) |
13 | | ecexg 8485 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑍 → [(𝑝 + 𝑞)]𝑇 ∈ V) |
14 | | elisset 2822 |
. . . . . . 7
⊢ ([(𝑝 + 𝑞)]𝑇 ∈ V → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) |
16 | 15 | biantrud 532 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))) |
17 | 16 | 2rexbidv 3231 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 (𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))) |
18 | 10, 17 | mpbid 231 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
19 | | 19.42v 1961 |
. . . . . . . 8
⊢
(∃𝑧((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
20 | 19 | bicomi 223 |
. . . . . . 7
⊢ (((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
21 | 20 | rexbii 3180 |
. . . . . 6
⊢
(∃𝑞 ∈
𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑞 ∈ 𝐵 ∃𝑧((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
22 | | rexcom4 3182 |
. . . . . 6
⊢
(∃𝑞 ∈
𝐵 ∃𝑧((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
23 | 21, 22 | bitri 274 |
. . . . 5
⊢
(∃𝑞 ∈
𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
24 | 23 | rexbii 3180 |
. . . 4
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝 ∈ 𝐴 ∃𝑧∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
25 | | rexcom4 3182 |
. . . 4
⊢
(∃𝑝 ∈
𝐴 ∃𝑧∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
26 | 24, 25 | bitri 274 |
. . 3
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
27 | 18, 26 | sylib 217 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
28 | | reeanv 3295 |
. . . . . 6
⊢
(∃𝑟 ∈
𝐴 ∃𝑠 ∈ 𝐴 (∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠 ∈ 𝐴 ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))) |
29 | | eceq1 8519 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅) |
30 | 29 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅 ↔ 𝑋 = [𝑟]𝑅)) |
31 | 30 | anbi1d 630 |
. . . . . . . . 9
⊢ (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑞]𝑆))) |
32 | | oveq1 7278 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞)) |
33 | 32 | eceq1d 8520 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇) |
34 | 33 | eqeq2d 2751 |
. . . . . . . . 9
⊢ (𝑝 = 𝑟 → (𝑧 = [(𝑝 + 𝑞)]𝑇 ↔ 𝑧 = [(𝑟 + 𝑞)]𝑇)) |
35 | 31, 34 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇))) |
36 | | eceq1 8519 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆) |
37 | 36 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆 ↔ 𝑌 = [𝑡]𝑆)) |
38 | 37 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆))) |
39 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡)) |
40 | 39 | eceq1d 8520 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇) |
41 | 40 | eqeq2d 2751 |
. . . . . . . . 9
⊢ (𝑞 = 𝑡 → (𝑧 = [(𝑟 + 𝑞)]𝑇 ↔ 𝑧 = [(𝑟 + 𝑡)]𝑇)) |
42 | 38, 41 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇))) |
43 | 35, 42 | cbvrex2vw 3395 |
. . . . . . 7
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇)) |
44 | | eceq1 8519 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅) |
45 | 44 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅 ↔ 𝑋 = [𝑠]𝑅)) |
46 | 45 | anbi1d 630 |
. . . . . . . . 9
⊢ (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑞]𝑆))) |
47 | | oveq1 7278 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞)) |
48 | 47 | eceq1d 8520 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇) |
49 | 48 | eqeq2d 2751 |
. . . . . . . . 9
⊢ (𝑝 = 𝑠 → (𝑤 = [(𝑝 + 𝑞)]𝑇 ↔ 𝑤 = [(𝑠 + 𝑞)]𝑇)) |
50 | 46, 49 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇))) |
51 | | eceq1 8519 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑢 → [𝑞]𝑆 = [𝑢]𝑆) |
52 | 51 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑢 → (𝑌 = [𝑞]𝑆 ↔ 𝑌 = [𝑢]𝑆)) |
53 | 52 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑞 = 𝑢 → ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆))) |
54 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑢 → (𝑠 + 𝑞) = (𝑠 + 𝑢)) |
55 | 54 | eceq1d 8520 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑢 → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + 𝑢)]𝑇) |
56 | 55 | eqeq2d 2751 |
. . . . . . . . 9
⊢ (𝑞 = 𝑢 → (𝑤 = [(𝑠 + 𝑞)]𝑇 ↔ 𝑤 = [(𝑠 + 𝑢)]𝑇)) |
57 | 53, 56 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑞 = 𝑢 → (((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))) |
58 | 50, 57 | cbvrex2vw 3395 |
. . . . . . 7
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑠 ∈ 𝐴 ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) |
59 | 43, 58 | anbi12i 627 |
. . . . . 6
⊢
((∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) ↔ (∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠 ∈ 𝐴 ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))) |
60 | 28, 59 | bitr4i 277 |
. . . . 5
⊢
(∃𝑟 ∈
𝐴 ∃𝑠 ∈ 𝐴 (∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇))) |
61 | | reeanv 3295 |
. . . . . . 7
⊢
(∃𝑡 ∈
𝐵 ∃𝑢 ∈ 𝐵 (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))) |
62 | | eropr.11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) |
63 | | eropr.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 Er 𝑈) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑅 Er 𝑈) |
65 | | eropr.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝐴 ⊆ 𝑈) |
67 | | simprll 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝐴) |
68 | 66, 67 | sseldd 3927 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝑈) |
69 | 64, 68 | erth 8530 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅)) |
70 | | eropr.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 Er 𝑉) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑆 Er 𝑉) |
72 | | eropr.8 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆ 𝑉) |
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝐵 ⊆ 𝑉) |
74 | | simprrl 778 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝐵) |
75 | 73, 74 | sseldd 3927 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝑉) |
76 | 71, 75 | erth 8530 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (𝑡𝑆𝑢 ↔ [𝑡]𝑆 = [𝑢]𝑆)) |
77 | 69, 76 | anbi12d 631 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆))) |
78 | | eropr.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 Er 𝑊) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑇 Er 𝑊) |
80 | | eropr.9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ⊆ 𝑊) |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝐶 ⊆ 𝑊) |
82 | | eropr.10 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → + :(𝐴 × 𝐵)⟶𝐶) |
84 | 83, 67, 74 | fovrnd 7438 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (𝑟 + 𝑡) ∈ 𝐶) |
85 | 81, 84 | sseldd 3927 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (𝑟 + 𝑡) ∈ 𝑊) |
86 | 79, 85 | erth 8530 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟 + 𝑡)𝑇(𝑠 + 𝑢) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇)) |
87 | 62, 77, 86 | 3imtr3d 293 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇)) |
88 | | eqeq2 2752 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = [(𝑠 + 𝑢)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇)) |
89 | 88 | biimprcd 249 |
. . . . . . . . . . . . 13
⊢ ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇 → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤)) |
90 | 87, 89 | syl6 35 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤))) |
91 | 90 | impd 411 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤)) |
92 | | eqeq1 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅)) |
93 | | eqeq1 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 = [𝑡]𝑆 → (𝑌 = [𝑢]𝑆 ↔ [𝑡]𝑆 = [𝑢]𝑆)) |
94 | 92, 93 | bi2anan9 636 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆))) |
95 | 94 | anbi1d 630 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))) |
96 | 95 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))) |
97 | | eqeq1 2744 |
. . . . . . . . . . . . 13
⊢ (𝑧 = [(𝑟 + 𝑡)]𝑇 → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤)) |
98 | 97 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤)) |
99 | 96, 98 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤))) |
100 | 91, 99 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤))) |
101 | 100 | impd 411 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤)) |
102 | 101 | anassrs 468 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤)) |
103 | 102 | rexlimdvva 3225 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) → (∃𝑡 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤)) |
104 | 61, 103 | syl5bir 242 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) → ((∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤)) |
105 | 104 | rexlimdvva 3225 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (∃𝑡 ∈ 𝐵 ((𝑋 = [𝑟]𝑅 ∧ 𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢 ∈ 𝐵 ((𝑋 = [𝑠]𝑅 ∧ 𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤)) |
106 | 60, 105 | syl5bir 242 |
. . . 4
⊢ (𝜑 → ((∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)) |
107 | 106 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ((∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)) |
108 | 107 | alrimivv 1935 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∀𝑧∀𝑤((∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)) |
109 | | eqeq1 2744 |
. . . . 5
⊢ (𝑧 = 𝑤 → (𝑧 = [(𝑝 + 𝑞)]𝑇 ↔ 𝑤 = [(𝑝 + 𝑞)]𝑇)) |
110 | 109 | anbi2d 629 |
. . . 4
⊢ (𝑧 = 𝑤 → (((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇))) |
111 | 110 | 2rexbidv 3231 |
. . 3
⊢ (𝑧 = 𝑤 → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇))) |
112 | 111 | eu4 2619 |
. 2
⊢
(∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (∃𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∀𝑧∀𝑤((∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))) |
113 | 27, 108, 112 | sylanbrc 583 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |