Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  relexpxpmin Structured version   Visualization version   GIF version

Theorem relexpxpmin 37028
 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.)
Assertion
Ref Expression
relexpxpmin (((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))

Proof of Theorem relexpxpmin
StepHypRef Expression
1 elnn0 11171 . . . . 5 (𝐾 ∈ ℕ0 ↔ (𝐾 ∈ ℕ ∨ 𝐾 = 0))
2 elnn0 11171 . . . . . . 7 (𝐽 ∈ ℕ0 ↔ (𝐽 ∈ ℕ ∨ 𝐽 = 0))
3 ifeqor 4082 . . . . . . . . . . 11 (if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽 ∨ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)
4 andi 907 . . . . . . . . . . . 12 ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ (if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽 ∨ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)) ↔ ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) ∨ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)))
54biimpi 205 . . . . . . . . . . 11 ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ (if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽 ∨ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)) → ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) ∨ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)))
63, 5mpan2 703 . . . . . . . . . 10 (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) ∨ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)))
7 eqtr 2629 . . . . . . . . . . 11 ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) → 𝐼 = 𝐽)
8 eqtr 2629 . . . . . . . . . . 11 ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾) → 𝐼 = 𝐾)
97, 8orim12i 537 . . . . . . . . . 10 (((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽) ∨ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)) → (𝐼 = 𝐽𝐼 = 𝐾))
10 relexpxpnnidm 37014 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℕ → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝐾) = (𝐴 × 𝐵)))
1110imp 444 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐾) = (𝐴 × 𝐵))
12113ad2antl3 1218 . . . . . . . . . . . . 13 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐾) = (𝐴 × 𝐵))
13 relexpxpnnidm 37014 . . . . . . . . . . . . . . . 16 (𝐽 ∈ ℕ → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝐽) = (𝐴 × 𝐵)))
1413imp 444 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = (𝐴 × 𝐵))
15143ad2antl2 1217 . . . . . . . . . . . . . 14 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = (𝐴 × 𝐵))
1615oveq1d 6564 . . . . . . . . . . . . 13 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐾))
17 simpl1 1057 . . . . . . . . . . . . . . 15 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐼 = 𝐽)
1817oveq2d 6565 . . . . . . . . . . . . . 14 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐼) = ((𝐴 × 𝐵)↑𝑟𝐽))
1918, 15eqtrd 2644 . . . . . . . . . . . . 13 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐼) = (𝐴 × 𝐵))
2012, 16, 193eqtr4d 2654 . . . . . . . . . . . 12 (((𝐼 = 𝐽𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
21203exp1 1275 . . . . . . . . . . 11 (𝐼 = 𝐽 → (𝐽 ∈ ℕ → (𝐾 ∈ ℕ → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
22143ad2antl2 1217 . . . . . . . . . . . . 13 (((𝐼 = 𝐾𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = (𝐴 × 𝐵))
23 simpl1 1057 . . . . . . . . . . . . . 14 (((𝐼 = 𝐾𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐼 = 𝐾)
2423eqcomd 2616 . . . . . . . . . . . . 13 (((𝐼 = 𝐾𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐾 = 𝐼)
2522, 24oveq12d 6567 . . . . . . . . . . . 12 (((𝐼 = 𝐾𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
26253exp1 1275 . . . . . . . . . . 11 (𝐼 = 𝐾 → (𝐽 ∈ ℕ → (𝐾 ∈ ℕ → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
2721, 26jaoi 393 . . . . . . . . . 10 ((𝐼 = 𝐽𝐼 = 𝐾) → (𝐽 ∈ ℕ → (𝐾 ∈ ℕ → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
286, 9, 273syl 18 . . . . . . . . 9 (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → (𝐽 ∈ ℕ → (𝐾 ∈ ℕ → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
2928com13 86 . . . . . . . 8 (𝐾 ∈ ℕ → (𝐽 ∈ ℕ → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
30 simp3 1056 . . . . . . . . . . 11 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))
31 simp2 1055 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐽 = 0)
32 simp1 1054 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐾 ∈ ℕ)
3332nngt0d 10941 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 0 < 𝐾)
3431, 33eqbrtrd 4605 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐽 < 𝐾)
3534iftrued 4044 . . . . . . . . . . 11 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐽)
3630, 35, 313eqtrd 2648 . . . . . . . . . 10 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐼 = 0)
37 simpr1 1060 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐴𝑈)
38 simpr2 1061 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐵𝑉)
39 xpexg 6858 . . . . . . . . . . . . . . 15 ((𝐴𝑈𝐵𝑉) → (𝐴 × 𝐵) ∈ V)
4037, 38, 39syl2anc 691 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (𝐴 × 𝐵) ∈ V)
41 dmexg 6989 . . . . . . . . . . . . . . 15 ((𝐴 × 𝐵) ∈ V → dom (𝐴 × 𝐵) ∈ V)
42 rnexg 6990 . . . . . . . . . . . . . . 15 ((𝐴 × 𝐵) ∈ V → ran (𝐴 × 𝐵) ∈ V)
4341, 42jca 553 . . . . . . . . . . . . . 14 ((𝐴 × 𝐵) ∈ V → (dom (𝐴 × 𝐵) ∈ V ∧ ran (𝐴 × 𝐵) ∈ V))
44 unexg 6857 . . . . . . . . . . . . . 14 ((dom (𝐴 × 𝐵) ∈ V ∧ ran (𝐴 × 𝐵) ∈ V) → (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) ∈ V)
4540, 43, 443syl 18 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) ∈ V)
46 simpl1 1057 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐾 ∈ ℕ)
4746nnnn0d 11228 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐾 ∈ ℕ0)
48 relexpiidm 37015 . . . . . . . . . . . . 13 (((dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) ∈ V ∧ 𝐾 ∈ ℕ0) → (( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)))↑𝑟𝐾) = ( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))))
4945, 47, 48syl2anc 691 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)))↑𝑟𝐾) = ( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))))
50 simpl2 1058 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐽 = 0)
5150oveq2d 6565 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = ((𝐴 × 𝐵)↑𝑟0))
52 relexp0g 13610 . . . . . . . . . . . . . . 15 ((𝐴 × 𝐵) ∈ V → ((𝐴 × 𝐵)↑𝑟0) = ( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))))
5340, 52syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟0) = ( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))))
5451, 53eqtrd 2644 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = ( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))))
5554oveq1d 6564 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = (( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)))↑𝑟𝐾))
56 simpl3 1059 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐼 = 0)
5756oveq2d 6565 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐼) = ((𝐴 × 𝐵)↑𝑟0))
5857, 53eqtrd 2644 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐼) = ( I ↾ (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))))
5949, 55, 583eqtr4d 2654 . . . . . . . . . . 11 (((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
6059ex 449 . . . . . . . . . 10 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = 0) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))
6136, 60syld3an3 1363 . . . . . . . . 9 ((𝐾 ∈ ℕ ∧ 𝐽 = 0 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))
62613exp 1256 . . . . . . . 8 (𝐾 ∈ ℕ → (𝐽 = 0 → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
6329, 62jaod 394 . . . . . . 7 (𝐾 ∈ ℕ → ((𝐽 ∈ ℕ ∨ 𝐽 = 0) → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
642, 63syl5bi 231 . . . . . 6 (𝐾 ∈ ℕ → (𝐽 ∈ ℕ0 → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
65 simp1 1054 . . . . . . . 8 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐾 = 0)
662biimpi 205 . . . . . . . . 9 (𝐽 ∈ ℕ0 → (𝐽 ∈ ℕ ∨ 𝐽 = 0))
67663ad2ant2 1076 . . . . . . . 8 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → (𝐽 ∈ ℕ ∨ 𝐽 = 0))
68 simp3 1056 . . . . . . . . 9 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾))
69 nn0nlt0 11196 . . . . . . . . . . . 12 (𝐽 ∈ ℕ0 → ¬ 𝐽 < 0)
70693ad2ant2 1076 . . . . . . . . . . 11 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ¬ 𝐽 < 0)
7165breq2d 4595 . . . . . . . . . . 11 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → (𝐽 < 𝐾𝐽 < 0))
7270, 71mtbird 314 . . . . . . . . . 10 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ¬ 𝐽 < 𝐾)
7372iffalsed 4047 . . . . . . . . 9 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → if(𝐽 < 𝐾, 𝐽, 𝐾) = 𝐾)
7468, 73, 653eqtrd 2648 . . . . . . . 8 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → 𝐼 = 0)
75133ad2ant2 1076 . . . . . . . . . . . . 13 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝐽) = (𝐴 × 𝐵)))
7675imp 444 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = (𝐴 × 𝐵))
7776oveq1d 6564 . . . . . . . . . . 11 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟0) = ((𝐴 × 𝐵)↑𝑟0))
78 simpl1 1057 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐾 = 0)
7978oveq2d 6565 . . . . . . . . . . 11 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟0))
80 simpl3 1059 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐼 = 0)
8180oveq2d 6565 . . . . . . . . . . 11 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐼) = ((𝐴 × 𝐵)↑𝑟0))
8277, 79, 813eqtr4d 2654 . . . . . . . . . 10 (((𝐾 = 0 ∧ 𝐽 ∈ ℕ ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
83823exp1 1275 . . . . . . . . 9 (𝐾 = 0 → (𝐽 ∈ ℕ → (𝐼 = 0 → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
84 simpr1 1060 . . . . . . . . . . . . 13 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐴𝑈)
85 simpr2 1061 . . . . . . . . . . . . 13 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐵𝑉)
8684, 85, 39syl2anc 691 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (𝐴 × 𝐵) ∈ V)
87 relexp0idm 37026 . . . . . . . . . . . 12 ((𝐴 × 𝐵) ∈ V → (((𝐴 × 𝐵)↑𝑟0)↑𝑟0) = ((𝐴 × 𝐵)↑𝑟0))
8886, 87syl 17 . . . . . . . . . . 11 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟0)↑𝑟0) = ((𝐴 × 𝐵)↑𝑟0))
89 simpl2 1058 . . . . . . . . . . . . 13 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐽 = 0)
9089oveq2d 6565 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐽) = ((𝐴 × 𝐵)↑𝑟0))
91 simpl1 1057 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐾 = 0)
9290, 91oveq12d 6567 . . . . . . . . . . 11 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = (((𝐴 × 𝐵)↑𝑟0)↑𝑟0))
93 simpl3 1059 . . . . . . . . . . . 12 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → 𝐼 = 0)
9493oveq2d 6565 . . . . . . . . . . 11 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → ((𝐴 × 𝐵)↑𝑟𝐼) = ((𝐴 × 𝐵)↑𝑟0))
9588, 92, 943eqtr4d 2654 . . . . . . . . . 10 (((𝐾 = 0 ∧ 𝐽 = 0 ∧ 𝐼 = 0) ∧ (𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
96953exp1 1275 . . . . . . . . 9 (𝐾 = 0 → (𝐽 = 0 → (𝐼 = 0 → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
9783, 96jaod 394 . . . . . . . 8 (𝐾 = 0 → ((𝐽 ∈ ℕ ∨ 𝐽 = 0) → (𝐼 = 0 → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
9865, 67, 74, 97syl3c 64 . . . . . . 7 ((𝐾 = 0 ∧ 𝐽 ∈ ℕ0𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))
99983exp 1256 . . . . . 6 (𝐾 = 0 → (𝐽 ∈ ℕ0 → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
10064, 99jaoi 393 . . . . 5 ((𝐾 ∈ ℕ ∨ 𝐾 = 0) → (𝐽 ∈ ℕ0 → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
1011, 100sylbi 206 . . . 4 (𝐾 ∈ ℕ0 → (𝐽 ∈ ℕ0 → (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
102101com13 86 . . 3 (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) → (𝐽 ∈ ℕ0 → (𝐾 ∈ ℕ0 → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))))
1031023imp 1249 . 2 ((𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0𝐾 ∈ ℕ0) → ((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)))
104103impcom 445 1 (((𝐴𝑈𝐵𝑉 ∧ (𝐴𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ∪ cun 3538   ∩ cin 3539  ∅c0 3874  ifcif 4036   class class class wbr 4583   I cid 4948   × cxp 5036  dom cdm 5038  ran crn 5039   ↾ cres 5040  (class class class)co 6549  0cc0 9815   < clt 9953  ℕcn 10897  ℕ0cn0 11169  ↑𝑟crelexp 13608 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-seq 12664  df-relexp 13609 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator