Metamath Proof Explorer

Theorem relexpxpmin

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

Ref Expression
Assertion relexpxpmin ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\wedge {A}\cap {B}\ne \varnothing \right)\wedge \left({I}=if\left({J}<{K},{J},{K}\right)\wedge {J}\in {ℕ}_{0}\wedge {K}\in {ℕ}_{0}\right)\right)\to \left(\left({A}×{B}\right){↑}_{r}{J}\right){↑}_{r}{K}=\left({A}×{B}\right){↑}_{r}{I}$

Proof

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