Step | Hyp | Ref
| Expression |
1 | | sopo 5630 |
. . . 4
⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵) |
2 | 1 | ralimi 3085 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝑆 Or 𝐵 → ∀𝑥 ∈ 𝐴 𝑆 Po 𝐵) |
3 | | weiunso.1 |
. . . 4
⊢ 𝐹 = (𝑤 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)) |
4 | | weiunso.2 |
. . . 4
⊢ 𝑇 = {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))} |
5 | 3, 4 | weiunpo 36378 |
. . 3
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Po 𝐵) → 𝑇 Po ∪
𝑥 ∈ 𝐴 𝐵) |
6 | 2, 5 | syl3an3 1165 |
. 2
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) → 𝑇 Po ∪
𝑥 ∈ 𝐴 𝐵) |
7 | | simplrl 776 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
8 | | simplrr 777 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
9 | | animorrl 981 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟))) |
10 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → 𝑦 = 𝑞) |
11 | 10 | fveq2d 6923 |
. . . . . . . 8
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → (𝐹‘𝑦) = (𝐹‘𝑞)) |
12 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → 𝑧 = 𝑟) |
13 | 12 | fveq2d 6923 |
. . . . . . . 8
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → (𝐹‘𝑧) = (𝐹‘𝑟)) |
14 | 11, 13 | breq12d 5182 |
. . . . . . 7
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝑞)𝑅(𝐹‘𝑟))) |
15 | 11, 13 | eqeq12d 2750 |
. . . . . . . 8
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝑞) = (𝐹‘𝑟))) |
16 | 11 | csbeq1d 3919 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑞) / 𝑥⦌𝑆) |
17 | 10, 16, 12 | breq123d 5183 |
. . . . . . . 8
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟)) |
18 | 15, 17 | anbi12d 631 |
. . . . . . 7
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟))) |
19 | 14, 18 | orbi12d 917 |
. . . . . 6
⊢ ((𝑦 = 𝑞 ∧ 𝑧 = 𝑟) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟)))) |
20 | 19, 4 | brab2a 5792 |
. . . . 5
⊢ (𝑞𝑇𝑟 ↔ ((𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟)))) |
21 | 7, 8, 9, 20 | syl21anbrc 1344 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → 𝑞𝑇𝑟) |
22 | 21 | 3mix1d 1336 |
. . 3
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
23 | | csbeq1 3918 |
. . . . . . . 8
⊢ (𝑠 = (𝐹‘𝑞) → ⦋𝑠 / 𝑥⦌𝑆 = ⦋(𝐹‘𝑞) / 𝑥⦌𝑆) |
24 | | soeq1 5632 |
. . . . . . . 8
⊢
(⦋𝑠 /
𝑥⦌𝑆 = ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 → (⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵)) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝑠 = (𝐹‘𝑞) → (⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵)) |
26 | | csbeq1 3918 |
. . . . . . . 8
⊢ (𝑠 = (𝐹‘𝑞) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
27 | | soeq2 5633 |
. . . . . . . 8
⊢
(⦋𝑠 /
𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 → (⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ (𝑠 = (𝐹‘𝑞) → (⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
29 | 25, 28 | bitrd 279 |
. . . . . 6
⊢ (𝑠 = (𝐹‘𝑞) → (⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
30 | | simpll3 1214 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) |
31 | | nfv 1913 |
. . . . . . . 8
⊢
Ⅎ𝑠 𝑆 Or 𝐵 |
32 | | nfcsb1v 3940 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 |
33 | | nfcsb1v 3940 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵 |
34 | 32, 33 | nfso 5617 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 |
35 | | csbeq1a 3929 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑠 → 𝑆 = ⦋𝑠 / 𝑥⦌𝑆) |
36 | | soeq1 5632 |
. . . . . . . . . 10
⊢ (𝑆 = ⦋𝑠 / 𝑥⦌𝑆 → (𝑆 Or 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Or 𝐵)) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 = 𝑠 → (𝑆 Or 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Or 𝐵)) |
38 | | csbeq1a 3929 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵) |
39 | | soeq2 5633 |
. . . . . . . . . 10
⊢ (𝐵 = ⦋𝑠 / 𝑥⦌𝐵 → (⦋𝑠 / 𝑥⦌𝑆 Or 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵)) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 = 𝑠 → (⦋𝑠 / 𝑥⦌𝑆 Or 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵)) |
41 | 37, 40 | bitrd 279 |
. . . . . . . 8
⊢ (𝑥 = 𝑠 → (𝑆 Or 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵)) |
42 | 31, 34, 41 | cbvralw 3307 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝑆 Or 𝐵 ↔ ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵) |
43 | 30, 42 | sylib 218 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵) |
44 | | simpl1 1191 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑅 We 𝐴) |
45 | | simpl2 1192 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑅 Se 𝐴) |
46 | 3 | weiunlem2 36377 |
. . . . . . . . . 10
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡)))) |
47 | 44, 45, 46 | syl2anc 583 |
. . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡)))) |
48 | 47 | simp1d 1142 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴) |
49 | | simprl 770 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
50 | 48, 49 | ffvelcdmd 7117 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝐹‘𝑞) ∈ 𝐴) |
51 | 50 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝐹‘𝑞) ∈ 𝐴) |
52 | 29, 43, 51 | rspcdva 3632 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
53 | | id 22 |
. . . . . . 7
⊢ (𝑡 = 𝑞 → 𝑡 = 𝑞) |
54 | | fveq2 6919 |
. . . . . . . 8
⊢ (𝑡 = 𝑞 → (𝐹‘𝑡) = (𝐹‘𝑞)) |
55 | 54 | csbeq1d 3919 |
. . . . . . 7
⊢ (𝑡 = 𝑞 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
56 | 53, 55 | eleq12d 2832 |
. . . . . 6
⊢ (𝑡 = 𝑞 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
57 | 47 | simp2d 1143 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵) |
58 | 57 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵) |
59 | | simplrl 776 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
60 | 56, 58, 59 | rspcdva 3632 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
61 | | id 22 |
. . . . . . . 8
⊢ (𝑡 = 𝑟 → 𝑡 = 𝑟) |
62 | | fveq2 6919 |
. . . . . . . . 9
⊢ (𝑡 = 𝑟 → (𝐹‘𝑡) = (𝐹‘𝑟)) |
63 | 62 | csbeq1d 3919 |
. . . . . . . 8
⊢ (𝑡 = 𝑟 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑟) / 𝑥⦌𝐵) |
64 | 61, 63 | eleq12d 2832 |
. . . . . . 7
⊢ (𝑡 = 𝑟 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑟 ∈ ⦋(𝐹‘𝑟) / 𝑥⦌𝐵)) |
65 | | simplrr 777 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
66 | 64, 58, 65 | rspcdva 3632 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑟 ∈ ⦋(𝐹‘𝑟) / 𝑥⦌𝐵) |
67 | | simpr 484 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝐹‘𝑞) = (𝐹‘𝑟)) |
68 | 67 | csbeq1d 3919 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑟) / 𝑥⦌𝐵) |
69 | 66, 68 | eleqtrrd 2841 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑟 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
70 | | solin 5636 |
. . . . 5
⊢
((⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 ∧ (𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 ∧ 𝑟 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) → (𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞)) |
71 | 52, 60, 69, 70 | syl12anc 836 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞)) |
72 | | simpllr 775 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
73 | 67 | anim1i 614 |
. . . . . . . 8
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟)) |
74 | 73 | olcd 873 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟))) |
75 | 72, 74, 20 | sylanbrc 582 |
. . . . . 6
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → 𝑞𝑇𝑟) |
76 | 75 | ex 412 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 → 𝑞𝑇𝑟)) |
77 | | idd 24 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞 = 𝑟 → 𝑞 = 𝑟)) |
78 | 65 | adantr 480 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
79 | 59 | adantr 480 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
80 | | simplr 768 |
. . . . . . . . . 10
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → (𝐹‘𝑞) = (𝐹‘𝑟)) |
81 | 80 | eqcomd 2740 |
. . . . . . . . 9
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → (𝐹‘𝑟) = (𝐹‘𝑞)) |
82 | 80 | csbeq1d 3919 |
. . . . . . . . . 10
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑟) / 𝑥⦌𝑆) |
83 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) |
84 | 82, 83 | breqdi 5184 |
. . . . . . . . 9
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞) |
85 | 81, 84 | jca 511 |
. . . . . . . 8
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞)) |
86 | 85 | olcd 873 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞))) |
87 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → 𝑦 = 𝑟) |
88 | 87 | fveq2d 6923 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → (𝐹‘𝑦) = (𝐹‘𝑟)) |
89 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → 𝑧 = 𝑞) |
90 | 89 | fveq2d 6923 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → (𝐹‘𝑧) = (𝐹‘𝑞)) |
91 | 88, 90 | breq12d 5182 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝑟)𝑅(𝐹‘𝑞))) |
92 | 88, 90 | eqeq12d 2750 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝑟) = (𝐹‘𝑞))) |
93 | 88 | csbeq1d 3919 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑟) / 𝑥⦌𝑆) |
94 | 87, 93, 89 | breq123d 5183 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞)) |
95 | 92, 94 | anbi12d 631 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞))) |
96 | 91, 95 | orbi12d 917 |
. . . . . . . 8
⊢ ((𝑦 = 𝑟 ∧ 𝑧 = 𝑞) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞)))) |
97 | 96, 4 | brab2a 5792 |
. . . . . . 7
⊢ (𝑟𝑇𝑞 ↔ ((𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞)))) |
98 | 78, 79, 86, 97 | syl21anbrc 1344 |
. . . . . 6
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟𝑇𝑞) |
99 | 98 | ex 412 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞 → 𝑟𝑇𝑞)) |
100 | 76, 77, 99 | 3orim123d 1444 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ((𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞))) |
101 | 71, 100 | mpd 15 |
. . 3
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
102 | | simplrr 777 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
103 | | simplrl 776 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
104 | | animorrl 981 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞))) |
105 | 102, 103,
104, 97 | syl21anbrc 1344 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → 𝑟𝑇𝑞) |
106 | 105 | 3mix3d 1338 |
. . 3
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
107 | | weso 5690 |
. . . . 5
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
108 | 44, 107 | syl 17 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑅 Or 𝐴) |
109 | | simprr 772 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
110 | 48, 109 | ffvelcdmd 7117 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝐹‘𝑟) ∈ 𝐴) |
111 | | solin 5636 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘𝑟) ∈ 𝐴)) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ (𝐹‘𝑞) = (𝐹‘𝑟) ∨ (𝐹‘𝑟)𝑅(𝐹‘𝑞))) |
112 | 108, 50, 110, 111 | syl12anc 836 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ (𝐹‘𝑞) = (𝐹‘𝑟) ∨ (𝐹‘𝑟)𝑅(𝐹‘𝑞))) |
113 | 22, 101, 106, 112 | mpjao3dan 1432 |
. 2
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
114 | 6, 113 | issod 5644 |
1
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) → 𝑇 Or ∪
𝑥 ∈ 𝐴 𝐵) |