Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem3 Structured version   Visualization version   GIF version

Theorem poimirlem3 33839
Description: Lemma for poimir 33869 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem4.1 (𝜑𝐾 ∈ ℕ)
poimirlem4.2 (𝜑𝑀 ∈ ℕ0)
poimirlem4.3 (𝜑𝑀 < 𝑁)
poimirlem3.4 (𝜑𝑇:(1...𝑀)⟶(0..^𝐾))
poimirlem3.5 (𝜑𝑈:(1...𝑀)–1-1-onto→(1...𝑀))
Assertion
Ref Expression
poimirlem3 (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))
Distinct variable groups:   𝑓,𝑖,𝑗,𝑝   𝜑,𝑗   𝑗,𝑀   𝑗,𝑁   𝑇,𝑗   𝑈,𝑗   𝜑,𝑖,𝑝   𝐵,𝑓,𝑖,𝑗   𝑓,𝐾,𝑖,𝑗,𝑝   𝑓,𝑀,𝑖,𝑝   𝑓,𝑁,𝑖,𝑝   𝑇,𝑓,𝑖,𝑝   𝑈,𝑓,𝑖,𝑝
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑝)

Proof of Theorem poimirlem3
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 poimirlem3.4 . . . . . . . . . . . . . . 15 (𝜑𝑇:(1...𝑀)⟶(0..^𝐾))
21ffnd 6226 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑀))
32adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀))
4 1ex 10291 . . . . . . . . . . . . . . . . 17 1 ∈ V
5 fnconstg 6277 . . . . . . . . . . . . . . . . 17 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
64, 5ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
7 c0ex 10289 . . . . . . . . . . . . . . . . 17 0 ∈ V
8 fnconstg 6277 . . . . . . . . . . . . . . . . 17 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
97, 8ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))
106, 9pm3.2i 462 . . . . . . . . . . . . . . 15 (((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
11 poimirlem3.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑈:(1...𝑀)–1-1-onto→(1...𝑀))
12 dff1o3 6328 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun 𝑈))
1312simprbi 490 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun 𝑈)
14 imain 6154 . . . . . . . . . . . . . . . . 17 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
1511, 13, 143syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
16 elfznn0 12643 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
1716nn0red 11601 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
1817ltp1d 11210 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1))
19 fzdisj 12578 . . . . . . . . . . . . . . . . . . 19 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
2018, 19syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
2120imaeq2d 5650 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅))
22 ima0 5665 . . . . . . . . . . . . . . . . 17 (𝑈 “ ∅) = ∅
2321, 22syl6eq 2815 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅)
2415, 23sylan9req 2820 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅)
25 fnun 6177 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
2610, 24, 25sylancr 581 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
27 imaundi 5730 . . . . . . . . . . . . . . . 16 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))
28 nn0p1nn 11581 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
29 nnuz 11926 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
3028, 29syl6eleq 2854 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ (ℤ‘1))
3116, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈ (ℤ‘1))
32 elfzuz3 12549 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ𝑗))
33 fzsplit2 12576 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑀 ∈ (ℤ𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
3431, 32, 33syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
3534eqcomd 2771 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀))
3635imaeq2d 5650 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀)))
37 f1ofo 6329 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀))
38 foima 6305 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀))
3911, 37, 383syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀))
4036, 39sylan9eqr 2821 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀))
4127, 40syl5eqr 2813 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀))
4241fneq2d 6162 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)))
4326, 42mpbid 223 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))
44 ovexd 6878 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V)
45 inidm 3984 . . . . . . . . . . . . 13 ((1...𝑀) ∩ (1...𝑀)) = (1...𝑀)
46 eqidd 2766 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇𝑛) = (𝑇𝑛))
47 eqidd 2766 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
483, 43, 44, 44, 45, 46, 47offval 7104 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
49 poimirlem4.2 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℕ0)
50 nn0p1nn 11581 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
5149, 50syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 + 1) ∈ ℕ)
5251nnzd 11731 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℤ)
53 uzid 11904 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ (ℤ‘(𝑀 + 1)))
54 peano2uz 11944 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ (ℤ‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
5552, 53, 543syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
56 poimirlem4.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 < 𝑁)
5749nn0zd 11730 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
58 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
5958nnzd 11731 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
60 zltp1le 11677 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
61 peano2z 11668 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
62 eluz 11903 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
6361, 62sylan 575 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
6460, 63bitr4d 273 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁𝑁 ∈ (ℤ‘(𝑀 + 1))))
6557, 59, 64syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 < 𝑁𝑁 ∈ (ℤ‘(𝑀 + 1))))
6656, 65mpbid 223 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
67 fzsplit2 12576 . . . . . . . . . . . . . . . . 17 ((((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
6855, 66, 67syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
69 fzsn 12593 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ ℤ → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
7052, 69syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
7170uneq1d 3930 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
7268, 71eqtrd 2799 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
7372xpeq1d 5308 . . . . . . . . . . . . . 14 (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}))
74 xpundir 5342 . . . . . . . . . . . . . . 15 (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
75 ovex 6876 . . . . . . . . . . . . . . . . 17 (𝑀 + 1) ∈ V
7675, 7xpsn 6600 . . . . . . . . . . . . . . . 16 ({(𝑀 + 1)} × {0}) = {⟨(𝑀 + 1), 0⟩}
7776uneq1i 3927 . . . . . . . . . . . . . . 15 (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
7874, 77eqtri 2787 . . . . . . . . . . . . . 14 (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
7973, 78syl6eq 2815 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8079adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8148, 80uneq12d 3932 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))))
82 unass 3934 . . . . . . . . . . 11 (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8381, 82syl6eqr 2817 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8449nn0red 11601 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ ℝ)
8584ltp1d 11210 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 < (𝑀 + 1))
8651nnred 11293 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 + 1) ∈ ℝ)
8784, 86ltnled 10440 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
8885, 87mpbid 223 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
89 elfzle2 12555 . . . . . . . . . . . . . . . . . . 19 ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀)
9088, 89nsyl 137 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀))
91 disjsn 4404 . . . . . . . . . . . . . . . . . 18 (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ↔ ¬ (𝑀 + 1) ∈ (1...𝑀))
9290, 91sylibr 225 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)
93 eqid 2765 . . . . . . . . . . . . . . . . . . 19 {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩}
9475, 7fsn 6595 . . . . . . . . . . . . . . . . . . 19 ({⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0} ↔ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩})
9593, 94mpbir 222 . . . . . . . . . . . . . . . . . 18 {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}
96 fun 6250 . . . . . . . . . . . . . . . . . 18 (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
9795, 96mpanl2 692 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
981, 92, 97syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
99 1z 11657 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℤ
100 nn0uz 11925 . . . . . . . . . . . . . . . . . . . . 21 0 = (ℤ‘0)
101 1m1e0 11346 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 1) = 0
102101fveq2i 6380 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘(1 − 1)) = (ℤ‘0)
103100, 102eqtr4i 2790 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘(1 − 1))
10449, 103syl6eleq 2854 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (ℤ‘(1 − 1)))
105 fzsuc2 12608 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℤ ∧ 𝑀 ∈ (ℤ‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
10699, 104, 105sylancr 581 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
107106eqcomd 2771 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
108 poimirlem4.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℕ)
109 lbfzo0 12719 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ (0..^𝐾) ↔ 𝐾 ∈ ℕ)
110108, 109sylibr 225 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ∈ (0..^𝐾))
111110snssd 4496 . . . . . . . . . . . . . . . . . 18 (𝜑 → {0} ⊆ (0..^𝐾))
112 ssequn2 3950 . . . . . . . . . . . . . . . . . 18 ({0} ⊆ (0..^𝐾) ↔ ((0..^𝐾) ∪ {0}) = (0..^𝐾))
113111, 112sylib 209 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾))
114107, 113feq23d 6220 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾)))
11598, 114mpbid 223 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
116115ffnd 6226 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
117116adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
118 fnconstg 6277 . . . . . . . . . . . . . . . . 17 (1 ∈ V → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)))
1194, 118ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗))
120 fnconstg 6277 . . . . . . . . . . . . . . . . 17 (0 ∈ V → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
1217, 120ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))
122119, 121pm3.2i 462 . . . . . . . . . . . . . . 15 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
12375, 75f1osn 6361 . . . . . . . . . . . . . . . . . . 19 {⟨(𝑀 + 1), (𝑀 + 1)⟩}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}
124 f1oun 6341 . . . . . . . . . . . . . . . . . . 19 (((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
125123, 124mpanl2 692 . . . . . . . . . . . . . . . . . 18 ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
12611, 92, 92, 125syl12anc 865 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
127 dff1o3 6328 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})))
128127simprbi 490 . . . . . . . . . . . . . . . . 17 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}))
129 imain 6154 . . . . . . . . . . . . . . . . 17 (Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
130126, 128, 1293syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
131 fzdisj 12578 . . . . . . . . . . . . . . . . . . 19 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
13218, 131syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
133132imaeq2d 5650 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅))
134 ima0 5665 . . . . . . . . . . . . . . . . 17 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅) = ∅
135133, 134syl6eq 2815 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
136130, 135sylan9req 2820 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
137 fnun 6177 . . . . . . . . . . . . . . 15 ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
138122, 136, 137sylancr 581 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
139 f1ofo 6329 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}))
140 foima 6305 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)}))
141126, 139, 1403syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)}))
142106imaeq2d 5650 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})))
143141, 142, 1063eqtr4d 2809 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1)))
144 peano2uz 11944 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ𝑗) → (𝑀 + 1) ∈ (ℤ𝑗))
14532, 144syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ (ℤ𝑗))
146 fzsplit2 12576 . . . . . . . . . . . . . . . . . . 19 (((𝑗 + 1) ∈ (ℤ‘1) ∧ (𝑀 + 1) ∈ (ℤ𝑗)) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
14731, 145, 146syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
148147imaeq2d 5650 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
149143, 148sylan9req 2820 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
150 imaundi 5730 . . . . . . . . . . . . . . . 16 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
151149, 150syl6eq 2815 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
152151fneq2d 6162 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)) ↔ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))))
153138, 152mpbird 248 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)))
154 ovexd 6878 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V)
155 inidm 3984 . . . . . . . . . . . . 13 ((1...(𝑀 + 1)) ∩ (1...(𝑀 + 1))) = (1...(𝑀 + 1))
156 eqidd 2766 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛))
157 eqidd 2766 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
158117, 153, 154, 154, 155, 156, 157offval 7104 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = (𝑛 ∈ (1...(𝑀 + 1)) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))))
159 ovexd 6878 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ V)
1607a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ V)
161107adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
162 fveq2 6377 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)))
16375snid 4368 . . . . . . . . . . . . . . . . . . . 20 (𝑀 + 1) ∈ {(𝑀 + 1)}
16475, 7fnsn 6127 . . . . . . . . . . . . . . . . . . . . 21 {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)}
165 fvun2 6461 . . . . . . . . . . . . . . . . . . . . 21 ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
166164, 165mp3an2 1573 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
167163, 166mpanr2 695 . . . . . . . . . . . . . . . . . . 19 ((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
1682, 92, 167syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
16975, 7fvsn 6641 . . . . . . . . . . . . . . . . . 18 ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)) = 0
170168, 169syl6eq 2815 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0)
171162, 170sylan9eqr 2821 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
172171adantlr 706 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
173 fveq2 6377 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)))
174 imadmrn 5660 . . . . . . . . . . . . . . . . . . . . . . . 24 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)})
17575, 75xpsn 6600 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝑀 + 1)} × {(𝑀 + 1)}) = {⟨(𝑀 + 1), (𝑀 + 1)⟩}
176175imaeq1i 5647 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)}))
177 dmxpid 5515 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
178177imaeq2i 5648 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
179176, 178eqtri 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
180 rnxpid 5752 . . . . . . . . . . . . . . . . . . . . . . . 24 ran ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
181174, 179, 1803eqtr3ri 2796 . . . . . . . . . . . . . . . . . . . . . . 23 {(𝑀 + 1)} = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
182 eluzp1p1 11915 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ (ℤ𝑗) → (𝑀 + 1) ∈ (ℤ‘(𝑗 + 1)))
183 eluzfz2 12559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 + 1) ∈ (ℤ‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
18432, 182, 1833syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
185184snssd 4496 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)))
186 imass2 5685 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
187185, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (0...𝑀) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
188181, 187syl5eqss 3811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
189 ssel 3757 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → ((𝑀 + 1) ∈ {(𝑀 + 1)} → (𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
190188, 163, 189mpisyl 21 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
191 elun2 3945 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
193 imaundir 5731 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
194192, 193syl6eleqr 2855 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
195194adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
196 fvun2 6461 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) ∧ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅ ∧ (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)))
197119, 121, 196mp3an12 1575 . . . . . . . . . . . . . . . . . 18 (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅ ∧ (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)))
198136, 195, 197syl2anc 579 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)))
1997fvconst2 6664 . . . . . . . . . . . . . . . . . . 19 ((𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
200194, 199syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
201200adantl 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
202198, 201eqtrd 2799 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0)
203173, 202sylan9eqr 2821 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0)
204172, 203oveq12d 6862 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0))
205 00id 10467 . . . . . . . . . . . . . 14 (0 + 0) = 0
206204, 205syl6eq 2815 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0)
207159, 160, 161, 206fmptapd 6632 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) = (𝑛 ∈ (1...(𝑀 + 1)) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))))
2082, 92jca 507 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅))
209 fvun1 6460 . . . . . . . . . . . . . . . . . . 19 ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
210164, 209mp3an2 1573 . . . . . . . . . . . . . . . . . 18 ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
211210anassrs 459 . . . . . . . . . . . . . . . . 17 (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
212208, 211sylan 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
213212adantlr 706 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
214 fvres 6396 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
215214eqcomd 2771 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛))
216 resundir 5589 . . . . . . . . . . . . . . . . . 18 (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
217 relxp 5297 . . . . . . . . . . . . . . . . . . . . . . 23 Rel ((𝑈 “ (1...𝑗)) × {1})
218 dmxpss 5750 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗))
219 imassrn 5661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ (1...𝑗)) ⊆ ran 𝑈
220218, 219sstri 3772 . . . . . . . . . . . . . . . . . . . . . . . 24 dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ ran 𝑈
221 f1of 6322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀))
222 frn 6231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀))
22311, 221, 2223syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ran 𝑈 ⊆ (1...𝑀))
224220, 223syl5ss 3774 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀))
225 relssres 5615 . . . . . . . . . . . . . . . . . . . . . . 23 ((Rel ((𝑈 “ (1...𝑗)) × {1}) ∧ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
226217, 224, 225sylancr 581 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
227226adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
228 imassrn 5661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
22975rnsnop 5803 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ran {⟨(𝑀 + 1), (𝑀 + 1)⟩} = {(𝑀 + 1)}
230228, 229sseqtri 3799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)}
231 ssrin 3999 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
232230, 231ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
233 incom 3969 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)})
234233, 92syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅)
235232, 234syl5sseq 3815 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅)
236 ss0 4138 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
237235, 236syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
238 fnconstg 6277 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
239 fnresdisj 6181 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅))
2404, 238, 239mp2b 10 . . . . . . . . . . . . . . . . . . . . . . 23 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
241237, 240sylib 209 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
242241adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
243227, 242uneq12d 3932 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅))
244 imaundir 5731 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
245244xpeq1i 5305 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1})
246 xpundir 5342 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
247245, 246eqtri 2787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
248247reseq1i 5563 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀))
249 resundir 5589 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)))
250248, 249eqtr2i 2788 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀))
251 un0 4131 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1})
252243, 250, 2513eqtr3g 2822 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
253 f1odm 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀))
25411, 253syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → dom 𝑈 = (1...𝑀))
255254ineq2d 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))
256255reseq2d 5567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))))
257 f1orel 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈)
258 resindm 5623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Rel 𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
25911, 257, 2583syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
260256, 259eqtr3d 2801 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
26134ineq2d 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))))
262 fzssp1 12594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1))
263 sseqin2 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
264262, 263mpbi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)
265264a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
266 incom 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))
267266, 132syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅)
268265, 267uneq12d 3932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅))
269 uncom 3921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
270 indi 4040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
271269, 270eqtr4i 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
272 un0 4131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀)
273268, 271, 2723eqtr3g 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀))
274261, 273eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀))
275274reseq2d 5567 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
276260, 275sylan9req 2820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
277276rneqd 5523 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)))
278 df-ima 5292 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))
279 df-ima 5292 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))
280277, 278, 2793eqtr4g 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀)))
281280xpeq1d 5308 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
282281reseq1d 5566 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)))
283 relxp 5297 . . . . . . . . . . . . . . . . . . . . . . . 24 Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
284 dmxpss 5750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀))
285 imassrn 5661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈
286284, 285sstri 3772 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈
287286, 223syl5ss 3774 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀))
288 relssres 5615 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∧ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
289283, 287, 288sylancr 581 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
290289adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
291282, 290eqtrd 2799 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
292 imassrn 5661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
293292, 229sseqtri 3799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)}
294 ssrin 3999 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
295293, 294ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
296295, 234syl5sseq 3815 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅)
297 ss0 4138 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
298296, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
299 fnconstg 6277 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
300 fnresdisj 6181 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅))
3017, 299, 300mp2b 10 . . . . . . . . . . . . . . . . . . . . . . 23 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
302298, 301sylib 209 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
303302adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
304291, 303uneq12d 3932 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅))
305193xpeq1i 5305 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0})
306 xpundir 5342 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
307305, 306eqtri 2787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
308307reseq1i 5563 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))
309 resundir 5589 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
310308, 309eqtr2i 2788 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))
311 un0 4131 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
312304, 310, 3113eqtr3g 2822 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
313252, 312uneq12d 3932 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
314216, 313syl5eq 2811 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
315314fveq1d 6379 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
316215, 315sylan9eqr 2821 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
317213, 316oveq12d 6862 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))
318317mpteq2dva 4905 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
319318uneq1d 3930 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
320158, 207, 3193eqtr2d 2805 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
321320uneq1d 3930 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
32283, 321eqtr4d 2802 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
323322csbeq1d 3700 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵)
324323eqeq2d 2775 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
325324rexbidva 3196 . . . . . 6 (𝜑 → (∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 ↔ ∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
326325ralbidv 3133 . . . . 5 (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 ↔ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
327326biimpd 220 . . . 4 (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 → ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
328 f1ofn 6323 . . . . . . . 8 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀))
32911, 328syl 17 . . . . . . 7 (𝜑𝑈 Fn (1...𝑀))
33075, 75fnsn 6127 . . . . . . . . 9 {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)}
331 fvun2 6461 . . . . . . . . 9 ((𝑈 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
332330, 331mp3an2 1573 . . . . . . . 8 ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
333163, 332mpanr2 695 . . . . . . 7 ((𝑈 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
334329, 92, 333syl2anc 579 . . . . . 6 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
33575, 75fvsn 6641 . . . . . 6 ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)) = (𝑀 + 1)
336334, 335syl6eq 2815 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))
337170, 336jca 507 . . . 4 (𝜑 → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))
338327, 337jctird 522 . . 3 (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))
339 3anass 1116 . . 3 ((∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))))
340338, 339syl6ibr 243 . 2 (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))))
3411, 95jctir 516 . . . . . 6 (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}))
342341, 92, 96syl2anc 579 . . . . 5 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
343342, 114mpbid 223 . . . 4 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
344 ovex 6876 . . . . 5 (0..^𝐾) ∈ V
345 ovex 6876 . . . . 5 (1...(𝑀 + 1)) ∈ V
346344, 345elmap 8091 . . . 4 ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
347343, 346sylibr 225 . . 3 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))))
348 ovex 6876 . . . . . . . 8 (1...𝑀) ∈ V
349 f1oexrnex 7315 . . . . . . . 8 ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V)
35011, 348, 349sylancl 580 . . . . . . 7 (𝜑𝑈 ∈ V)
351 snex 5066 . . . . . . 7 {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V
352 unexg 7159 . . . . . . 7 ((𝑈 ∈ V ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
353350, 351, 352sylancl 580 . . . . . 6 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
354 f1oeq1 6312 . . . . . . 7 (𝑓 = (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
355354elabg 3505 . . . . . 6 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
356353, 355syl 17 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
357 f1oeq23 6315 . . . . . 6 (((1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}) ∧ (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
358106, 106, 357syl2anc 579 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
359356, 358bitrd 270 . . . 4 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
360126, 359mpbird 248 . . 3 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})
361 opelxpi 5316 . . 3 (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) ∧ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) → ⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}))
362347, 360, 361syl2anc 579 . 2 (𝜑 → ⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}))
363340, 362jctild 521 1 (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  {cab 2751  wral 3055  wrex 3056  Vcvv 3350  csb 3693  cun 3732  cin 3733  wss 3734  c0 4081  {csn 4336  cop 4342   class class class wbr 4811  cmpt 4890   × cxp 5277  ccnv 5278  dom cdm 5279  ran crn 5280  cres 5281  cima 5282  Rel wrel 5284  Fun wfun 6064   Fn wfn 6065  wf 6066  ontowfo 6068  1-1-ontowf1o 6069  cfv 6070  (class class class)co 6844  𝑓 cof 7095  𝑚 cmap 8062  0cc0 10191  1c1 10192   + caddc 10194   < clt 10330  cle 10331  cmin 10522  cn 11276  0cn0 11540  cz 11626  cuz 11889  ...cfz 12536  ..^cfzo 12676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-er 7949  df-map 8064  df-en 8163  df-dom 8164  df-sdom 8165  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-nn 11277  df-n0 11541  df-z 11627  df-uz 11890  df-fz 12537  df-fzo 12677
This theorem is referenced by:  poimirlem4  33840
  Copyright terms: Public domain W3C validator