Metamath Proof Explorer

Theorem relexpxpmin

Description: The composition of powers of a Cartesian product of non-disjoint sets is the Cartesian product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion relexpxpmin ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
2 elnn0 ⊢ ( 𝐽 ∈ ℕ0 ↔ ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) )
3 ifeqor ⊢ ( if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ∨ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 )
4 andi ⊢ ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ ( if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ∨ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) ) ↔ ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ) ∨ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) ) )
5 4 biimpi ⊢ ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ ( if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ∨ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) ) → ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ) ∨ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) ) )
6 3 5 mpan2 ⊢ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ) ∨ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) ) )
7 eqtr ⊢ ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ) → 𝐼 = 𝐽 )
8 eqtr ⊢ ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) → 𝐼 = 𝐾 )
9 7 8 orim12i ⊢ ( ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 ) ∨ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 ) ) → ( 𝐼 = 𝐽 ∨ 𝐼 = 𝐾 ) )
10 relexpxpnnidm ⊢ ( 𝐾 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐾 ) = ( 𝐴 × 𝐵 ) ) )
11 10 imp ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐾 ) = ( 𝐴 × 𝐵 ) )
12 11 3ad2antl3 ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐾 ) = ( 𝐴 × 𝐵 ) )
13 relexpxpnnidm ⊢ ( 𝐽 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( 𝐴 × 𝐵 ) ) )
14 13 imp ⊢ ( ( 𝐽 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( 𝐴 × 𝐵 ) )
15 14 3ad2antl2 ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( 𝐴 × 𝐵 ) )
16 15 oveq1d ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐾 ) )
17 simpl1 ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐼 = 𝐽 )
18 17 oveq2d ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) )
19 18 15 eqtrd ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) = ( 𝐴 × 𝐵 ) )
20 12 16 19 3eqtr4d ⊢ ( ( ( 𝐼 = 𝐽 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )
21 20 3exp1 ⊢ ( 𝐼 = 𝐽 → ( 𝐽 ∈ ℕ → ( 𝐾 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
22 14 3ad2antl2 ⊢ ( ( ( 𝐼 = 𝐾 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( 𝐴 × 𝐵 ) )
23 simpl1 ⊢ ( ( ( 𝐼 = 𝐾 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐼 = 𝐾 )
24 23 eqcomd ⊢ ( ( ( 𝐼 = 𝐾 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐾 = 𝐼 )
25 22 24 oveq12d ⊢ ( ( ( 𝐼 = 𝐾 ∧ 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )
26 25 3exp1 ⊢ ( 𝐼 = 𝐾 → ( 𝐽 ∈ ℕ → ( 𝐾 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
27 21 26 jaoi ⊢ ( ( 𝐼 = 𝐽 ∨ 𝐼 = 𝐾 ) → ( 𝐽 ∈ ℕ → ( 𝐾 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
28 6 9 27 3syl ⊢ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( 𝐽 ∈ ℕ → ( 𝐾 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
29 28 com13 ⊢ ( 𝐾 ∈ ℕ → ( 𝐽 ∈ ℕ → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
30 simp3 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) )
31 simp2 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐽 = 0 )
32 simp1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐾 ∈ ℕ )
33 32 nngt0d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 0 < 𝐾 )
34 31 33 eqbrtrd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐽 < 𝐾 )
35 34 iftrued ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐽 )
36 30 35 31 3eqtrd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐼 = 0 )
37 simpr1 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐴 ∈ 𝑈 )
38 simpr2 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐵 ∈ 𝑉 )
39 37 38 xpexd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ∈ V )
40 dmexg ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → dom ( 𝐴 × 𝐵 ) ∈ V )
41 rnexg ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ran ( 𝐴 × 𝐵 ) ∈ V )
42 40 41 jca ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( dom ( 𝐴 × 𝐵 ) ∈ V ∧ ran ( 𝐴 × 𝐵 ) ∈ V ) )
43 unexg ⊢ ( ( dom ( 𝐴 × 𝐵 ) ∈ V ∧ ran ( 𝐴 × 𝐵 ) ∈ V ) → ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ∈ V )
44 39 42 43 3syl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ∈ V )
45 simpl1 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐾 ∈ ℕ )
46 45 nnnn0d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐾 ∈ ℕ0 )
47 relexpiidm ⊢ ( ( ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ∈ V ∧ 𝐾 ∈ ℕ0 ) → ( ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) ↑𝑟 𝐾 ) = ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) )
48 44 46 47 syl2anc ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) ↑𝑟 𝐾 ) = ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) )
49 simpl2 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐽 = 0 )
50 49 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
51 relexp0g ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) = ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) )
52 39 51 syl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) = ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) )
53 50 52 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) )
54 53 oveq1d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) ↑𝑟 𝐾 ) )
55 simpl3 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐼 = 0 )
56 55 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
57 56 52 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) = ( I ↾ ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) ) )
58 48 54 57 3eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )
59 58 ex ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) )
60 36 59 syld3an3 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) )
61 60 3exp ⊢ ( 𝐾 ∈ ℕ → ( 𝐽 = 0 → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
62 29 61 jaod ⊢ ( 𝐾 ∈ ℕ → ( ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
63 2 62 biimtrid ⊢ ( 𝐾 ∈ ℕ → ( 𝐽 ∈ ℕ0 → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
64 simp1 ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐾 = 0 )
65 2 biimpi ⊢ ( 𝐽 ∈ ℕ0 → ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) )
66 65 3ad2ant2 ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) )
67 simp3 ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) )
68 nn0nlt0 ⊢ ( 𝐽 ∈ ℕ0 → ¬ 𝐽 < 0 )
69 68 3ad2ant2 ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ¬ 𝐽 < 0 )
70 64 breq2d ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( 𝐽 < 𝐾 ↔ 𝐽 < 0 ) )
71 69 70 mtbird ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ¬ 𝐽 < 𝐾 )
72 71 iffalsed ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) = 𝐾 )
73 67 72 64 3eqtrd ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → 𝐼 = 0 )
74 13 3ad2ant2 ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( 𝐴 × 𝐵 ) ) )
75 74 imp ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( 𝐴 × 𝐵 ) )
76 75 oveq1d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 0 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
77 simpl1 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐾 = 0 )
78 77 oveq2d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 0 ) )
79 simpl3 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐼 = 0 )
80 79 oveq2d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
81 76 78 80 3eqtr4d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )
82 81 3exp1 ⊢ ( 𝐾 = 0 → ( 𝐽 ∈ ℕ → ( 𝐼 = 0 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
83 simpr1 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐴 ∈ 𝑈 )
84 simpr2 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐵 ∈ 𝑉 )
85 83 84 xpexd ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ∈ V )
86 relexp0idm ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) ↑𝑟 0 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
87 85 86 syl ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) ↑𝑟 0 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
88 simpl2 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐽 = 0 )
89 88 oveq2d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
90 simpl1 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐾 = 0 )
91 89 90 oveq12d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) ↑𝑟 0 ) )
92 simpl3 ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → 𝐼 = 0 )
93 92 oveq2d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 0 ) )
94 87 91 93 3eqtr4d ⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )
95 94 3exp1 ⊢ ( 𝐾 = 0 → ( 𝐽 = 0 → ( 𝐼 = 0 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
96 82 95 jaod ⊢ ( 𝐾 = 0 → ( ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) → ( 𝐼 = 0 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
97 64 66 73 96 syl3c ⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ0 ∧ 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) )
98 97 3exp ⊢ ( 𝐾 = 0 → ( 𝐽 ∈ ℕ0 → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
99 63 98 jaoi ⊢ ( ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) → ( 𝐽 ∈ ℕ0 → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
100 1 99 sylbi ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐽 ∈ ℕ0 → ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) ) ) )
101 100 3imp31 ⊢ ( ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) ) )
102 101 impcom ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( 𝐼 = if ( 𝐽 < 𝐾 , 𝐽 , 𝐾 ) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝐼 ) )