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