Metamath Proof Explorer

Theorem relexp01min

Description: With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020)

Ref Expression
Assertion relexp01min ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ∧ ( 𝐽 ∈ { 0 , 1 } ∧ 𝐾 ∈ { 0 , 1 } ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )

Proof

Step Hyp Ref Expression
1 elpri ⊢ ( 𝐽 ∈ { 0 , 1 } → ( 𝐽 = 0 ∨ 𝐽 = 1 ) )
2 elpri ⊢ ( 𝐾 ∈ { 0 , 1 } → ( 𝐾 = 0 ∨ 𝐾 = 1 ) )
3 dmresi ⊢ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
4 rnresi ⊢ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
5 3 4 uneq12i ⊢ ( dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∪ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( dom 𝑅 ∪ ran 𝑅 ) ∪ ( dom 𝑅 ∪ ran 𝑅 ) )
6 unidm ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) ∪ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
7 5 6 eqtri ⊢ ( dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∪ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( dom 𝑅 ∪ ran 𝑅 )
8 7 reseq2i ⊢ ( I ↾ ( dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∪ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
9 simp1 ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐽 = 0 )
10 9 oveq2d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( 𝑅 ↑𝑟 0 ) )
11 simp3l ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝑅 ∈ 𝑉 )
12 relexp0g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
13 11 12 syl ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
14 10 13 eqtrd ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
15 simp2 ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐾 = 0 )
16 14 15 oveq12d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 0 ) )
17 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
18 rnexg ⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ∈ V )
19 unexg ⊢ ( ( dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V ) → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
20 17 18 19 syl2anc ⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
21 20 resiexd ⊢ ( 𝑅 ∈ 𝑉 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
22 relexp0g ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 0 ) = ( I ↾ ( dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∪ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ) )
23 11 21 22 3syl ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 0 ) = ( I ↾ ( dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∪ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ) )
24 16 23 eqtrd ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( I ↾ ( dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∪ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ) )
25 simp3r ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) )
26 0re ⊢ 0 ∈ ℝ
27 26 ltnri ⊢ ¬ 0 < 0
28 9 15 breq12d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝐽 < 𝐾 ↔ 0 < 0 ) )
29 27 28 mtbiri ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ¬ 𝐽 < 𝐾 )
30 29 iffalsed ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 )
31 25 30 15 3eqtrd ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = 0 )
32 31 oveq2d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( 𝑅 ↑𝑟 0 ) )
33 32 13 eqtrd ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
34 8 24 33 3eqtr4a ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
35 34 3exp ⊢ ( 𝐽 = 0 → ( 𝐾 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
36 simp1 ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐽 = 1 )
37 36 oveq2d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( 𝑅 ↑𝑟 1 ) )
38 simp3l ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝑅 ∈ 𝑉 )
39 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
40 38 39 syl ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
41 37 40 eqtrd ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = 𝑅 )
42 simp2 ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐾 = 0 )
43 41 42 oveq12d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 0 ) )
44 simp3r ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) )
45 0lt1 ⊢ 0 < 1
46 1re ⊢ 1 ∈ ℝ
47 26 46 ltnsymi ⊢ ( 0 < 1 → ¬ 1 < 0 )
48 45 47 mp1i ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ¬ 1 < 0 )
49 36 42 breq12d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝐽 < 𝐾 ↔ 1 < 0 ) )
50 48 49 mtbird ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ¬ 𝐽 < 𝐾 )
51 50 iffalsed ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 )
52 44 51 42 3eqtrd ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = 0 )
53 52 oveq2d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( 𝑅 ↑𝑟 0 ) )
54 43 53 eqtr4d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 0 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
55 54 3exp ⊢ ( 𝐽 = 1 → ( 𝐾 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
56 35 55 jaoi ⊢ ( ( 𝐽 = 0 ∨ 𝐽 = 1 ) → ( 𝐾 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
57 ovex ⊢ ( 𝑅 ↑𝑟 0 ) ∈ V
58 relexp1g ⊢ ( ( 𝑅 ↑𝑟 0 ) ∈ V → ( ( 𝑅 ↑𝑟 0 ) ↑𝑟 1 ) = ( 𝑅 ↑𝑟 0 ) )
59 57 58 mp1i ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 0 ) ↑𝑟 1 ) = ( 𝑅 ↑𝑟 0 ) )
60 simp1 ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐽 = 0 )
61 60 oveq2d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( 𝑅 ↑𝑟 0 ) )
62 simp2 ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐾 = 1 )
63 61 62 oveq12d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝑅 ↑𝑟 0 ) ↑𝑟 1 ) )
64 simp3r ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) )
65 60 62 breq12d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝐽 < 𝐾 ↔ 0 < 1 ) )
66 45 65 mpbiri ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐽 < 𝐾 )
67 66 iftrued ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 )
68 64 67 60 3eqtrd ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = 0 )
69 68 oveq2d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( 𝑅 ↑𝑟 0 ) )
70 59 63 69 3eqtr4d ⊢ ( ( 𝐽 = 0 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
71 70 3exp ⊢ ( 𝐽 = 0 → ( 𝐾 = 1 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
72 simp1 ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐽 = 1 )
73 72 oveq2d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( 𝑅 ↑𝑟 1 ) )
74 simp3l ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝑅 ∈ 𝑉 )
75 74 39 syl ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
76 73 75 eqtrd ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = 𝑅 )
77 simp2 ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐾 = 1 )
78 76 77 oveq12d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 1 ) )
79 simp3r ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) )
80 46 ltnri ⊢ ¬ 1 < 1
81 72 77 breq12d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝐽 < 𝐾 ↔ 1 < 1 ) )
82 80 81 mtbiri ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ¬ 𝐽 < 𝐾 )
83 82 iffalsed ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 )
84 79 83 77 3eqtrd ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → 𝐼 = 1 )
85 84 oveq2d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( 𝑅 ↑𝑟 1 ) )
86 78 85 eqtr4d ⊢ ( ( 𝐽 = 1 ∧ 𝐾 = 1 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
87 86 3exp ⊢ ( 𝐽 = 1 → ( 𝐾 = 1 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
88 71 87 jaoi ⊢ ( ( 𝐽 = 0 ∨ 𝐽 = 1 ) → ( 𝐾 = 1 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
89 56 88 jaod ⊢ ( ( 𝐽 = 0 ∨ 𝐽 = 1 ) → ( ( 𝐾 = 0 ∨ 𝐾 = 1 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
90 89 imp ⊢ ( ( ( 𝐽 = 0 ∨ 𝐽 = 1 ) ∧ ( 𝐾 = 0 ∨ 𝐾 = 1 ) ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
91 1 2 90 syl2an ⊢ ( ( 𝐽 ∈ { 0 , 1 } ∧ 𝐾 ∈ { 0 , 1 } ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
92 91 impcom ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) ∧ ( 𝐽 ∈ { 0 , 1 } ∧ 𝐾 ∈ { 0 , 1 } ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )