Step | Hyp | Ref
| Expression |
1 | | sopo 5627 |
. . . 4
⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵) |
2 | 1 | ralimi 3089 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝑆 Or 𝐵 → ∀𝑥 ∈ 𝐴 𝑆 Po 𝐵) |
3 | | weiun.1 |
. . . 4
⊢ 𝐹 = (𝑤 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)) |
4 | | weiun.2 |
. . . 4
⊢ 𝑇 = {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))} |
5 | 3, 4 | weiunpo 36431 |
. . 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 | 3, 4 | weiunlem1 36428 |
. . . . 5
⊢ (𝑞𝑇𝑟 ↔ ((𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟)))) |
11 | 7, 8, 9, 10 | syl21anbrc 1344 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → 𝑞𝑇𝑟) |
12 | 11 | 3mix1d 1336 |
. . 3
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑟)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
13 | | csbeq1 3924 |
. . . . . . 7
⊢ (𝑠 = (𝐹‘𝑞) → ⦋𝑠 / 𝑥⦌𝑆 = ⦋(𝐹‘𝑞) / 𝑥⦌𝑆) |
14 | | csbeq1 3924 |
. . . . . . 7
⊢ (𝑠 = (𝐹‘𝑞) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
15 | 13, 14 | soeq12d 5631 |
. . . . . 6
⊢ (𝑠 = (𝐹‘𝑞) → (⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
16 | | simpll3 1214 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) |
17 | | nfv 1913 |
. . . . . . . 8
⊢
Ⅎ𝑠 𝑆 Or 𝐵 |
18 | | nfcsb1v 3946 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 |
19 | | nfcsb1v 3946 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵 |
20 | 18, 19 | nfso 5614 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵 |
21 | | csbeq1a 3935 |
. . . . . . . . 9
⊢ (𝑥 = 𝑠 → 𝑆 = ⦋𝑠 / 𝑥⦌𝑆) |
22 | | csbeq1a 3935 |
. . . . . . . . 9
⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵) |
23 | 21, 22 | soeq12d 5631 |
. . . . . . . 8
⊢ (𝑥 = 𝑠 → (𝑆 Or 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵)) |
24 | 17, 20, 23 | cbvralw 3312 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝑆 Or 𝐵 ↔ ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵) |
25 | 16, 24 | sylib 218 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Or ⦋𝑠 / 𝑥⦌𝐵) |
26 | | simpl1 1191 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑅 We 𝐴) |
27 | | simpl2 1192 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑅 Se 𝐴) |
28 | 3, 4, 26, 27 | weiunlem2 36429 |
. . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡))) |
29 | 28 | simp1d 1142 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴) |
30 | | simprl 770 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
31 | 29, 30 | ffvelcdmd 7119 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝐹‘𝑞) ∈ 𝐴) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝐹‘𝑞) ∈ 𝐴) |
33 | 15, 25, 32 | rspcdva 3636 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
34 | | id 22 |
. . . . . . 7
⊢ (𝑡 = 𝑞 → 𝑡 = 𝑞) |
35 | | fveq2 6920 |
. . . . . . . 8
⊢ (𝑡 = 𝑞 → (𝐹‘𝑡) = (𝐹‘𝑞)) |
36 | 35 | csbeq1d 3925 |
. . . . . . 7
⊢ (𝑡 = 𝑞 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
37 | 34, 36 | eleq12d 2838 |
. . . . . 6
⊢ (𝑡 = 𝑞 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
38 | 28 | simp2d 1143 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵) |
39 | 38 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵) |
40 | | simplrl 776 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
41 | 37, 39, 40 | rspcdva 3636 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
42 | | id 22 |
. . . . . . . 8
⊢ (𝑡 = 𝑟 → 𝑡 = 𝑟) |
43 | | fveq2 6920 |
. . . . . . . . 9
⊢ (𝑡 = 𝑟 → (𝐹‘𝑡) = (𝐹‘𝑟)) |
44 | 43 | csbeq1d 3925 |
. . . . . . . 8
⊢ (𝑡 = 𝑟 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑟) / 𝑥⦌𝐵) |
45 | 42, 44 | eleq12d 2838 |
. . . . . . 7
⊢ (𝑡 = 𝑟 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑟 ∈ ⦋(𝐹‘𝑟) / 𝑥⦌𝐵)) |
46 | | simplrr 777 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
47 | 45, 39, 46 | rspcdva 3636 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑟 ∈ ⦋(𝐹‘𝑟) / 𝑥⦌𝐵) |
48 | | simpr 484 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝐹‘𝑞) = (𝐹‘𝑟)) |
49 | 48 | csbeq1d 3925 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑟) / 𝑥⦌𝐵) |
50 | 47, 49 | eleqtrrd 2847 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → 𝑟 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
51 | | solin 5634 |
. . . . 5
⊢
((⦋(𝐹‘𝑞) / 𝑥⦌𝑆 Or ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 ∧ (𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵 ∧ 𝑟 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) → (𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞)) |
52 | 33, 41, 50, 51 | syl12anc 836 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞)) |
53 | | simpllr 775 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
54 | 48 | anim1i 614 |
. . . . . . . 8
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟)) |
55 | 54 | olcd 873 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ ((𝐹‘𝑞) = (𝐹‘𝑟) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟))) |
56 | 53, 55, 10 | sylanbrc 582 |
. . . . . 6
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟) → 𝑞𝑇𝑟) |
57 | 56 | ex 412 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 → 𝑞𝑇𝑟)) |
58 | | idd 24 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞 = 𝑟 → 𝑞 = 𝑟)) |
59 | 46 | adantr 480 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
60 | 40 | adantr 480 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
61 | | simplr 768 |
. . . . . . . . . 10
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → (𝐹‘𝑞) = (𝐹‘𝑟)) |
62 | 61 | eqcomd 2746 |
. . . . . . . . 9
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → (𝐹‘𝑟) = (𝐹‘𝑞)) |
63 | 61 | csbeq1d 3925 |
. . . . . . . . . 10
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → ⦋(𝐹‘𝑞) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑟) / 𝑥⦌𝑆) |
64 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) |
65 | 63, 64 | breqdi 5181 |
. . . . . . . . 9
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞) |
66 | 62, 65 | jca 511 |
. . . . . . . 8
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞)) |
67 | 66 | olcd 873 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞))) |
68 | 3, 4 | weiunlem1 36428 |
. . . . . . 7
⊢ (𝑟𝑇𝑞 ↔ ((𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞)))) |
69 | 59, 60, 67, 68 | syl21anbrc 1344 |
. . . . . 6
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) ∧ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → 𝑟𝑇𝑞) |
70 | 69 | ex 412 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞 → 𝑟𝑇𝑞)) |
71 | 57, 58, 70 | 3orim123d 1444 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → ((𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑞) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞))) |
72 | 52, 71 | mpd 15 |
. . 3
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑞) = (𝐹‘𝑟)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
73 | | simplrr 777 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
74 | | simplrl 776 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
75 | | animorrl 981 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → ((𝐹‘𝑟)𝑅(𝐹‘𝑞) ∨ ((𝐹‘𝑟) = (𝐹‘𝑞) ∧ 𝑟⦋(𝐹‘𝑟) / 𝑥⦌𝑆𝑞))) |
76 | 73, 74, 75, 68 | syl21anbrc 1344 |
. . . 4
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → 𝑟𝑇𝑞) |
77 | 76 | 3mix3d 1338 |
. . 3
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) ∧ (𝐹‘𝑟)𝑅(𝐹‘𝑞)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
78 | | weso 5691 |
. . . . 5
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
79 | 26, 78 | syl 17 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑅 Or 𝐴) |
80 | | simprr 772 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
81 | 29, 80 | ffvelcdmd 7119 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝐹‘𝑟) ∈ 𝐴) |
82 | | solin 5634 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘𝑟) ∈ 𝐴)) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ (𝐹‘𝑞) = (𝐹‘𝑟) ∨ (𝐹‘𝑟)𝑅(𝐹‘𝑞))) |
83 | 79, 31, 81, 82 | syl12anc 836 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → ((𝐹‘𝑞)𝑅(𝐹‘𝑟) ∨ (𝐹‘𝑞) = (𝐹‘𝑟) ∨ (𝐹‘𝑟)𝑅(𝐹‘𝑞))) |
84 | 12, 72, 77, 83 | mpjao3dan 1432 |
. 2
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) ∧ (𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) → (𝑞𝑇𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟𝑇𝑞)) |
85 | 6, 84 | issod 5642 |
1
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) → 𝑇 Or ∪
𝑥 ∈ 𝐴 𝐵) |