Proof of Theorem relexp01min
Step | Hyp | Ref
| Expression |
1 | | elpri 4608 |
. . 3
⊢ (𝐽 ∈ {0, 1} → (𝐽 = 0 ∨ 𝐽 = 1)) |
2 | | elpri 4608 |
. . 3
⊢ (𝐾 ∈ {0, 1} → (𝐾 = 0 ∨ 𝐾 = 1)) |
3 | | dmresi 6005 |
. . . . . . . . . . 11
⊢ dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
4 | | rnresi 6027 |
. . . . . . . . . . 11
⊢ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
5 | 3, 4 | uneq12i 4121 |
. . . . . . . . . 10
⊢ (dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) ∪ ran ( I ↾
(dom 𝑅 ∪ ran 𝑅))) = ((dom 𝑅 ∪ ran 𝑅) ∪ (dom 𝑅 ∪ ran 𝑅)) |
6 | | unidm 4112 |
. . . . . . . . . 10
⊢ ((dom
𝑅 ∪ ran 𝑅) ∪ (dom 𝑅 ∪ ran 𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
7 | 5, 6 | eqtri 2764 |
. . . . . . . . 9
⊢ (dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) ∪ ran ( I ↾
(dom 𝑅 ∪ ran 𝑅))) = (dom 𝑅 ∪ ran 𝑅) |
8 | 7 | reseq2i 5934 |
. . . . . . . 8
⊢ ( I
↾ (dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∪ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅)))) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)) |
9 | | simp1 1136 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 0) |
10 | 9 | oveq2d 7373 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
11 | | simp3l 1201 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝑅 ∈ 𝑉) |
12 | | relexp0g 14907 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
14 | 10, 13 | eqtrd 2776 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
15 | | simp2 1137 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 0) |
16 | 14, 15 | oveq12d 7375 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟0)) |
17 | | dmexg 7840 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
18 | | rnexg 7841 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V) |
19 | 17, 18 | unexd 7688 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
20 | 19 | resiexd 7166 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V) |
21 | | relexp0g 14907 |
. . . . . . . . . 10
⊢ (( I
↾ (dom 𝑅 ∪ ran
𝑅)) ∈ V → (( I
↾ (dom 𝑅 ∪ ran
𝑅))↑𝑟0) = ( I ↾
(dom ( I ↾ (dom 𝑅
∪ ran 𝑅)) ∪ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅))))) |
22 | 11, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟0) = ( I ↾
(dom ( I ↾ (dom 𝑅
∪ ran 𝑅)) ∪ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅))))) |
23 | 16, 22 | eqtrd 2776 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = ( I ↾ (dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∪ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅))))) |
24 | | simp3r 1202 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
25 | | 0re 11157 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
26 | 25 | ltnri 11264 |
. . . . . . . . . . . . 13
⊢ ¬ 0
< 0 |
27 | 9, 15 | breq12d 5118 |
. . . . . . . . . . . . 13
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 0 < 0)) |
28 | 26, 27 | mtbiri 326 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 𝐽 < 𝐾) |
29 | 28 | iffalsed 4497 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) |
30 | 24, 29, 15 | 3eqtrd 2780 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 0) |
31 | 30 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
32 | 31, 13 | eqtrd 2776 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
33 | 8, 23, 32 | 3eqtr4a 2802 |
. . . . . . 7
⊢ ((𝐽 = 0 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
34 | 33 | 3exp 1119 |
. . . . . 6
⊢ (𝐽 = 0 → (𝐾 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
35 | | simp1 1136 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 1) |
36 | 35 | oveq2d 7373 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟1)) |
37 | | simp3l 1201 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝑅 ∈ 𝑉) |
38 | 37 | relexp1d 14914 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟1) = 𝑅) |
39 | 36, 38 | eqtrd 2776 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = 𝑅) |
40 | | simp2 1137 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 0) |
41 | 39, 40 | oveq12d 7375 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟0)) |
42 | | simp3r 1202 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
43 | | 0lt1 11677 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
44 | | 1re 11155 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
45 | 25, 44 | ltnsymi 11274 |
. . . . . . . . . . . . 13
⊢ (0 < 1
→ ¬ 1 < 0) |
46 | 43, 45 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 1 < 0) |
47 | 35, 40 | breq12d 5118 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 1 < 0)) |
48 | 46, 47 | mtbird 324 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 𝐽 < 𝐾) |
49 | 48 | iffalsed 4497 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) |
50 | 42, 49, 40 | 3eqtrd 2780 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 0) |
51 | 50 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
52 | 41, 51 | eqtr4d 2779 |
. . . . . . 7
⊢ ((𝐽 = 1 ∧ 𝐾 = 0 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
53 | 52 | 3exp 1119 |
. . . . . 6
⊢ (𝐽 = 1 → (𝐾 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
54 | 34, 53 | jaoi 855 |
. . . . 5
⊢ ((𝐽 = 0 ∨ 𝐽 = 1) → (𝐾 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
55 | | ovex 7390 |
. . . . . . . . 9
⊢ (𝑅↑𝑟0)
∈ V |
56 | | relexp1g 14911 |
. . . . . . . . 9
⊢ ((𝑅↑𝑟0)
∈ V → ((𝑅↑𝑟0)↑𝑟1)
= (𝑅↑𝑟0)) |
57 | 55, 56 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟0)↑𝑟1)
= (𝑅↑𝑟0)) |
58 | | simp1 1136 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 0) |
59 | 58 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
60 | | simp2 1137 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 1) |
61 | 59, 60 | oveq12d 7375 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = ((𝑅↑𝑟0)↑𝑟1)) |
62 | | simp3r 1202 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
63 | 58, 60 | breq12d 5118 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 0 < 1)) |
64 | 43, 63 | mpbiri 257 |
. . . . . . . . . . 11
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 < 𝐾) |
65 | 64 | iftrued 4494 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) |
66 | 62, 65, 58 | 3eqtrd 2780 |
. . . . . . . . 9
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 0) |
67 | 66 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
68 | 57, 61, 67 | 3eqtr4d 2786 |
. . . . . . 7
⊢ ((𝐽 = 0 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
69 | 68 | 3exp 1119 |
. . . . . 6
⊢ (𝐽 = 0 → (𝐾 = 1 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
70 | | simp1 1136 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐽 = 1) |
71 | 70 | oveq2d 7373 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟1)) |
72 | | simp3l 1201 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝑅 ∈ 𝑉) |
73 | 72 | relexp1d 14914 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟1) = 𝑅) |
74 | 71, 73 | eqtrd 2776 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐽) = 𝑅) |
75 | | simp2 1137 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐾 = 1) |
76 | 74, 75 | oveq12d 7375 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟1)) |
77 | | simp3r 1202 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) |
78 | 44 | ltnri 11264 |
. . . . . . . . . . . 12
⊢ ¬ 1
< 1 |
79 | 70, 75 | breq12d 5118 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝐽 < 𝐾 ↔ 1 < 1)) |
80 | 78, 79 | mtbiri 326 |
. . . . . . . . . . 11
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ¬ 𝐽 < 𝐾) |
81 | 80 | iffalsed 4497 |
. . . . . . . . . 10
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) |
82 | 77, 81, 75 | 3eqtrd 2780 |
. . . . . . . . 9
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → 𝐼 = 1) |
83 | 82 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟1)) |
84 | 76, 83 | eqtr4d 2779 |
. . . . . . 7
⊢ ((𝐽 = 1 ∧ 𝐾 = 1 ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
85 | 84 | 3exp 1119 |
. . . . . 6
⊢ (𝐽 = 1 → (𝐾 = 1 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
86 | 69, 85 | jaoi 855 |
. . . . 5
⊢ ((𝐽 = 0 ∨ 𝐽 = 1) → (𝐾 = 1 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
87 | 54, 86 | jaod 857 |
. . . 4
⊢ ((𝐽 = 0 ∨ 𝐽 = 1) → ((𝐾 = 0 ∨ 𝐾 = 1) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
88 | 87 | imp 407 |
. . 3
⊢ (((𝐽 = 0 ∨ 𝐽 = 1) ∧ (𝐾 = 0 ∨ 𝐾 = 1)) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
89 | 1, 2, 88 | syl2an 596 |
. 2
⊢ ((𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1}) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
90 | 89 | impcom 408 |
1
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) ∧ (𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1})) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |