Proof of Theorem relexp01min
Step | Hyp | Ref
| Expression |
1 | | elpri 4563 |
. . 3
⊢ (𝐽 ∈ {0, 1} → (𝐽 = 0 ∨ 𝐽 = 1)) |
2 | | elpri 4563 |
. . 3
⊢ (𝐾 ∈ {0, 1} → (𝐾 = 0 ∨ 𝐾 = 1)) |
3 | | dmresi 5921 |
. . . . . . . . . . 11
⊢ dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
4 | | rnresi 5943 |
. . . . . . . . . . 11
⊢ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
5 | 3, 4 | uneq12i 4075 |
. . . . . . . . . 10
⊢ (dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) ∪ ran ( I ↾
(dom 𝑅 ∪ ran 𝑅))) = ((dom 𝑅 ∪ ran 𝑅) ∪ (dom 𝑅 ∪ ran 𝑅)) |
6 | | unidm 4066 |
. . . . . . . . . 10
⊢ ((dom
𝑅 ∪ ran 𝑅) ∪ (dom 𝑅 ∪ ran 𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
7 | 5, 6 | eqtri 2765 |
. . . . . . . . 9
⊢ (dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) ∪ ran ( I ↾
(dom 𝑅 ∪ ran 𝑅))) = (dom 𝑅 ∪ ran 𝑅) |
8 | 7 | reseq2i 5848 |
. . . . . . . 8
⊢ ( I
↾ (dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∪ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅)))) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)) |
9 | | simp1 1138 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 0) |
10 | 9 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
11 | | simp3l 1203 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝑅 ∈ 𝑉) |
12 | | relexp0g 14585 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
14 | 10, 13 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
15 | | simp2 1139 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 0) |
16 | 14, 15 | oveq12d 7231 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟0)) |
17 | | dmexg 7681 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
18 | | rnexg 7682 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V) |
19 | | unexg 7534 |
. . . . . . . . . . . 12
⊢ ((dom
𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
20 | 17, 18, 19 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
21 | 20 | resiexd 7032 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V) |
22 | | relexp0g 14585 |
. . . . . . . . . 10
⊢ (( I
↾ (dom 𝑅 ∪ ran
𝑅)) ∈ V → (( I
↾ (dom 𝑅 ∪ ran
𝑅))↑𝑟0) = ( I ↾
(dom ( I ↾ (dom 𝑅
∪ ran 𝑅)) ∪ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅))))) |
23 | 11, 21, 22 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟0) = ( I ↾
(dom ( I ↾ (dom 𝑅
∪ ran 𝑅)) ∪ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅))))) |
24 | 16, 23 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = ( I ↾ (dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∪ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅))))) |
25 | | simp3r 1204 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
26 | | 0re 10835 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
27 | 26 | ltnri 10941 |
. . . . . . . . . . . . 13
⊢ ¬ 0
< 0 |
28 | 9, 15 | breq12d 5066 |
. . . . . . . . . . . . 13
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 0 < 0)) |
29 | 27, 28 | mtbiri 330 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 𝐽 < 𝐾) |
30 | 29 | iffalsed 4450 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) |
31 | 25, 30, 15 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 0) |
32 | 31 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
33 | 32, 13 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
34 | 8, 24, 33 | 3eqtr4a 2804 |
. . . . . . 7
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
35 | 34 | 3exp 1121 |
. . . . . 6
⊢ (𝐽 = 0 → (𝐾 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
36 | | simp1 1138 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 1) |
37 | 36 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟1)) |
38 | | simp3l 1203 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝑅 ∈ 𝑉) |
39 | | relexp1g 14589 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟1) = 𝑅) |
41 | 37, 40 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = 𝑅) |
42 | | simp2 1139 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 0) |
43 | 41, 42 | oveq12d 7231 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟0)) |
44 | | simp3r 1204 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
45 | | 0lt1 11354 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
46 | | 1re 10833 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
47 | 26, 46 | ltnsymi 10951 |
. . . . . . . . . . . . 13
⊢ (0 < 1
→ ¬ 1 < 0) |
48 | 45, 47 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 1 < 0) |
49 | 36, 42 | breq12d 5066 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 1 < 0)) |
50 | 48, 49 | mtbird 328 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 𝐽 < 𝐾) |
51 | 50 | iffalsed 4450 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) |
52 | 44, 51, 42 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 0) |
53 | 52 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
54 | 43, 53 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
55 | 54 | 3exp 1121 |
. . . . . 6
⊢ (𝐽 = 1 → (𝐾 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
56 | 35, 55 | jaoi 857 |
. . . . 5
⊢ ((𝐽 = 0 ∨ 𝐽 = 1) → (𝐾 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
57 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑅↑𝑟0)
∈ V |
58 | | relexp1g 14589 |
. . . . . . . . 9
⊢ ((𝑅↑𝑟0)
∈ V → ((𝑅↑𝑟0)↑𝑟1)
= (𝑅↑𝑟0)) |
59 | 57, 58 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟0)↑𝑟1)
= (𝑅↑𝑟0)) |
60 | | simp1 1138 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 0) |
61 | 60 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
62 | | simp2 1139 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 1) |
63 | 61, 62 | oveq12d 7231 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = ((𝑅↑𝑟0)↑𝑟1)) |
64 | | simp3r 1204 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
65 | 60, 62 | breq12d 5066 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 0 < 1)) |
66 | 45, 65 | mpbiri 261 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 < 𝐾) |
67 | 66 | iftrued 4447 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) |
68 | 64, 67, 60 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 0) |
69 | 68 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
70 | 59, 63, 69 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
71 | 70 | 3exp 1121 |
. . . . . 6
⊢ (𝐽 = 0 → (𝐾 = 1 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
72 | | simp1 1138 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 1) |
73 | 72 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟1)) |
74 | | simp3l 1203 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝑅 ∈ 𝑉) |
75 | 74, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟1) = 𝑅) |
76 | 73, 75 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = 𝑅) |
77 | | simp2 1139 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 1) |
78 | 76, 77 | oveq12d 7231 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟1)) |
79 | | simp3r 1204 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
80 | 46 | ltnri 10941 |
. . . . . . . . . . . 12
⊢ ¬ 1
< 1 |
81 | 72, 77 | breq12d 5066 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 1 < 1)) |
82 | 80, 81 | mtbiri 330 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 𝐽 < 𝐾) |
83 | 82 | iffalsed 4450 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) |
84 | 79, 83, 77 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 1) |
85 | 84 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟1)) |
86 | 78, 85 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
87 | 86 | 3exp 1121 |
. . . . . 6
⊢ (𝐽 = 1 → (𝐾 = 1 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
88 | 71, 87 | jaoi 857 |
. . . . 5
⊢ ((𝐽 = 0 ∨ 𝐽 = 1) → (𝐾 = 1 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
89 | 56, 88 | jaod 859 |
. . . 4
⊢ ((𝐽 = 0 ∨ 𝐽 = 1) → ((𝐾 = 0 ∨ 𝐾 = 1) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
90 | 89 | imp 410 |
. . 3
⊢ (((𝐽 = 0 ∨ 𝐽 = 1) ∧ (𝐾 = 0 ∨ 𝐾 = 1)) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
91 | 1, 2, 90 | syl2an 599 |
. 2
⊢ ((𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1}) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
92 | 91 | impcom 411 |
1
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) ∧ (𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1})) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |