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

Theorem poimirlem3 34445
 Description: Lemma for poimir 34475 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 6383 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑀))
32adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀))
4 1ex 10483 . . . . . . . . . . . . . . . . 17 1 ∈ V
5 fnconstg 6435 . . . . . . . . . . . . . . . . 17 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
64, 5ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
7 c0ex 10481 . . . . . . . . . . . . . . . . 17 0 ∈ V
8 fnconstg 6435 . . . . . . . . . . . . . . . . 17 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
97, 8ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))
106, 9pm3.2i 471 . . . . . . . . . . . . . . 15 (((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
11 poimirlem3.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑈:(1...𝑀)–1-1-onto→(1...𝑀))
12 dff1o3 6489 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun 𝑈))
1312simprbi 497 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun 𝑈)
14 imain 6309 . . . . . . . . . . . . . . . . 17 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
1511, 13, 143syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
16 elfznn0 12850 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
1716nn0red 11804 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
1817ltp1d 11418 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1))
19 fzdisj 12784 . . . . . . . . . . . . . . . . . . 19 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
2018, 19syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
2120imaeq2d 5806 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅))
22 ima0 5821 . . . . . . . . . . . . . . . . 17 (𝑈 “ ∅) = ∅
2321, 22syl6eq 2847 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅)
2415, 23sylan9req 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅)
25 fnun 6333 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
2610, 24, 25sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
27 imaundi 5884 . . . . . . . . . . . . . . . 16 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))
28 nn0p1nn 11784 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
29 nnuz 12130 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
3028, 29syl6eleq 2893 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ (ℤ‘1))
3116, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈ (ℤ‘1))
32 elfzuz3 12755 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ𝑗))
33 fzsplit2 12782 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑀 ∈ (ℤ𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
3431, 32, 33syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
3534eqcomd 2801 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀))
3635imaeq2d 5806 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀)))
37 f1ofo 6490 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀))
38 foima 6463 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀))
3911, 37, 383syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀))
4036, 39sylan9eqr 2853 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀))
4127, 40syl5eqr 2845 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀))
4241fneq2d 6317 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)))
4326, 42mpbid 233 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))
44 ovexd 7050 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V)
45 inidm 4115 . . . . . . . . . . . . 13 ((1...𝑀) ∩ (1...𝑀)) = (1...𝑀)
46 eqidd 2796 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇𝑛) = (𝑇𝑛))
47 eqidd 2796 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
483, 43, 44, 44, 45, 46, 47offval 7274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
49 poimirlem4.2 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℕ0)
50 nn0p1nn 11784 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
5149, 50syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 + 1) ∈ ℕ)
5251nnzd 11935 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℤ)
53 uzid 12108 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ (ℤ‘(𝑀 + 1)))
54 peano2uz 12150 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ (ℤ‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
5552, 53, 543syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
56 poimirlem4.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 < 𝑁)
5749nn0zd 11934 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
58 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
5958nnzd 11935 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
60 zltp1le 11881 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
61 peano2z 11872 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
62 eluz 12107 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
6361, 62sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
6460, 63bitr4d 283 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁𝑁 ∈ (ℤ‘(𝑀 + 1))))
6557, 59, 64syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 < 𝑁𝑁 ∈ (ℤ‘(𝑀 + 1))))
6656, 65mpbid 233 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
67 fzsplit2 12782 . . . . . . . . . . . . . . . . 17 ((((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
6855, 66, 67syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
69 fzsn 12799 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ ℤ → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
7052, 69syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
7170uneq1d 4059 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
7268, 71eqtrd 2831 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
7372xpeq1d 5472 . . . . . . . . . . . . . 14 (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}))
74 xpundir 5507 . . . . . . . . . . . . . . 15 (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
75 ovex 7048 . . . . . . . . . . . . . . . . 17 (𝑀 + 1) ∈ V
7675, 7xpsn 6766 . . . . . . . . . . . . . . . 16 ({(𝑀 + 1)} × {0}) = {⟨(𝑀 + 1), 0⟩}
7776uneq1i 4056 . . . . . . . . . . . . . . 15 (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
7874, 77eqtri 2819 . . . . . . . . . . . . . 14 (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
7973, 78syl6eq 2847 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8079adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8148, 80uneq12d 4061 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))))
82 unass 4063 . . . . . . . . . . 11 (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8381, 82syl6eqr 2849 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8449nn0red 11804 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ ℝ)
8584ltp1d 11418 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 < (𝑀 + 1))
8651nnred 11501 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 + 1) ∈ ℝ)
8784, 86ltnled 10634 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
8885, 87mpbid 233 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
89 elfzle2 12761 . . . . . . . . . . . . . . . . . . 19 ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀)
9088, 89nsyl 142 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀))
91 disjsn 4554 . . . . . . . . . . . . . . . . . 18 (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ↔ ¬ (𝑀 + 1) ∈ (1...𝑀))
9290, 91sylibr 235 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)
93 eqid 2795 . . . . . . . . . . . . . . . . . . 19 {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩}
9475, 7fsn 6760 . . . . . . . . . . . . . . . . . . 19 ({⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0} ↔ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩})
9593, 94mpbir 232 . . . . . . . . . . . . . . . . . 18 {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}
96 fun 6408 . . . . . . . . . . . . . . . . . 18 (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
9795, 96mpanl2 697 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
981, 92, 97syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
99 1z 11861 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℤ
100 nn0uz 12129 . . . . . . . . . . . . . . . . . . . . 21 0 = (ℤ‘0)
101 1m1e0 11557 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 1) = 0
102101fveq2i 6541 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘(1 − 1)) = (ℤ‘0)
103100, 102eqtr4i 2822 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘(1 − 1))
10449, 103syl6eleq 2893 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (ℤ‘(1 − 1)))
105 fzsuc2 12815 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℤ ∧ 𝑀 ∈ (ℤ‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
10699, 104, 105sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
107106eqcomd 2801 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
108 poimirlem4.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℕ)
109 lbfzo0 12927 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ (0..^𝐾) ↔ 𝐾 ∈ ℕ)
110108, 109sylibr 235 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ∈ (0..^𝐾))
111110snssd 4649 . . . . . . . . . . . . . . . . . 18 (𝜑 → {0} ⊆ (0..^𝐾))
112 ssequn2 4080 . . . . . . . . . . . . . . . . . 18 ({0} ⊆ (0..^𝐾) ↔ ((0..^𝐾) ∪ {0}) = (0..^𝐾))
113111, 112sylib 219 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾))
114107, 113feq23d 6377 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾)))
11598, 114mpbid 233 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
116115ffnd 6383 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
117116adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
118 fnconstg 6435 . . . . . . . . . . . . . . . . 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 6435 . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . 15 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
12375, 75f1osn 6522 . . . . . . . . . . . . . . . . . . 19 {⟨(𝑀 + 1), (𝑀 + 1)⟩}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}
124 f1oun 6502 . . . . . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . . . . . 18 ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
12611, 92, 92, 125syl12anc 833 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
127 dff1o3 6489 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})))
128127simprbi 497 . . . . . . . . . . . . . . . . 17 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}))
129 imain 6309 . . . . . . . . . . . . . . . . 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 12784 . . . . . . . . . . . . . . . . . . 19 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
13218, 131syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
133132imaeq2d 5806 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅))
134 ima0 5821 . . . . . . . . . . . . . . . . 17 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅) = ∅
135133, 134syl6eq 2847 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
136130, 135sylan9req 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
137 fnun 6333 . . . . . . . . . . . . . . 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 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
139 f1ofo 6490 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}))
140 foima 6463 . . . . . . . . . . . . . . . . . . 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 5806 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})))
143141, 142, 1063eqtr4d 2841 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1)))
144 peano2uz 12150 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ𝑗) → (𝑀 + 1) ∈ (ℤ𝑗))
14532, 144syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ (ℤ𝑗))
146 fzsplit2 12782 . . . . . . . . . . . . . . . . . . 19 (((𝑗 + 1) ∈ (ℤ‘1) ∧ (𝑀 + 1) ∈ (ℤ𝑗)) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
14731, 145, 146syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
148147imaeq2d 5806 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
149143, 148sylan9req 2852 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
150 imaundi 5884 . . . . . . . . . . . . . . . 16 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
151149, 150syl6eq 2847 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
152151fneq2d 6317 . . . . . . . . . . . . . 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 258 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)))
154 ovexd 7050 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V)
155 inidm 4115 . . . . . . . . . . . . 13 ((1...(𝑀 + 1)) ∩ (1...(𝑀 + 1))) = (1...(𝑀 + 1))
156 eqidd 2796 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛))
157 eqidd 2796 . . . . . . . . . . . . 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 7274 . . . . . . . . . . . 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 7050 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ V)
1607a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ V)
161107adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
162 fveq2 6538 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)))
16375snid 4506 . . . . . . . . . . . . . . . . . . . 20 (𝑀 + 1) ∈ {(𝑀 + 1)}
16475, 7fnsn 6282 . . . . . . . . . . . . . . . . . . . . 21 {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)}
165 fvun2 6622 . . . . . . . . . . . . . . . . . . . . 21 ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
166164, 165mp3an2 1441 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
167163, 166mpanr2 700 . . . . . . . . . . . . . . . . . . 19 ((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
1682, 92, 167syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
16975, 7fvsn 6806 . . . . . . . . . . . . . . . . . 18 ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)) = 0
170168, 169syl6eq 2847 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0)
171162, 170sylan9eqr 2853 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
172171adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
173 fveq2 6538 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)))
174 imadmrn 5816 . . . . . . . . . . . . . . . . . . . . . . . 24 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)})
17575, 75xpsn 6766 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝑀 + 1)} × {(𝑀 + 1)}) = {⟨(𝑀 + 1), (𝑀 + 1)⟩}
176175imaeq1i 5803 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)}))
177 dmxpid 5682 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
178177imaeq2i 5804 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
179176, 178eqtri 2819 . . . . . . . . . . . . . . . . . . . . . . . 24 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
180 rnxpid 5906 . . . . . . . . . . . . . . . . . . . . . . . 24 ran ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
181174, 179, 1803eqtr3ri 2828 . . . . . . . . . . . . . . . . . . . . . . 23 {(𝑀 + 1)} = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
182 eluzp1p1 12119 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ (ℤ𝑗) → (𝑀 + 1) ∈ (ℤ‘(𝑗 + 1)))
183 eluzfz2 12765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 + 1) ∈ (ℤ‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
18432, 182, 1833syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
185184snssd 4649 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)))
186 imass2 5841 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
187185, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (0...𝑀) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
188181, 187eqsstrid 3936 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
189 ssel 3883 . . . . . . . . . . . . . . . . . . . . . 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 4074 . . . . . . . . . . . . . . . . . . . . 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 5885 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
194192, 193syl6eleqr 2894 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
195194adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
196 fvun2 6622 . . . . . . . . . . . . . . . . . . 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 1443 . . . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)))
1997fvconst2 6833 . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
202198, 201eqtrd 2831 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0)
203173, 202sylan9eqr 2853 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0)
204172, 203oveq12d 7034 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0))
205 00id 10662 . . . . . . . . . . . . . 14 (0 + 0) = 0
206204, 205syl6eq 2847 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0)
207159, 160, 161, 206fmptapd 6796 . . . . . . . . . . . 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 512 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅))
209 fvun1 6621 . . . . . . . . . . . . . . . . . . 19 ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
210164, 209mp3an2 1441 . . . . . . . . . . . . . . . . . 18 ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
211210anassrs 468 . . . . . . . . . . . . . . . . 17 (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
212208, 211sylan 580 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
213212adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
214 fvres 6557 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
215214eqcomd 2801 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛))
216 resundir 5749 . . . . . . . . . . . . . . . . . 18 (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
217 relxp 5461 . . . . . . . . . . . . . . . . . . . . . . 23 Rel ((𝑈 “ (1...𝑗)) × {1})
218 dmxpss 5904 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗))
219 imassrn 5817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ (1...𝑗)) ⊆ ran 𝑈
220218, 219sstri 3898 . . . . . . . . . . . . . . . . . . . . . . . 24 dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ ran 𝑈
221 f1of 6483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀))
222 frn 6388 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀))
22311, 221, 2223syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ran 𝑈 ⊆ (1...𝑀))
224220, 223syl5ss 3900 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀))
225 relssres 5774 . . . . . . . . . . . . . . . . . . . . . . 23 ((Rel ((𝑈 “ (1...𝑗)) × {1}) ∧ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
226217, 224, 225sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
227226adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
228 imassrn 5817 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
22975rnsnop 5956 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ran {⟨(𝑀 + 1), (𝑀 + 1)⟩} = {(𝑀 + 1)}
230228, 229sseqtri 3924 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)}
231 ssrin 4130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
232230, 231ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
233 incom 4099 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)})
234233, 92syl5eq 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅)
235232, 234sseqtrid 3940 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅)
236 ss0 4272 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
237235, 236syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
238 fnconstg 6435 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
239 fnresdisj 6337 . . . . . . . . . . . . . . . . . . . . . . . 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 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
242241adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
243227, 242uneq12d 4061 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅))
244 imaundir 5885 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
245244xpeq1i 5469 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1})
246 xpundir 5507 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
247245, 246eqtri 2819 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
248247reseq1i 5730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀))
249 resundir 5749 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)))
250248, 249eqtr2i 2820 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀))
251 un0 4264 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1})
252243, 250, 2513eqtr3g 2854 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
253 f1odm 6487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀))
25411, 253syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → dom 𝑈 = (1...𝑀))
255254ineq2d 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))
256255reseq2d 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))))
257 f1orel 6486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈)
258 resindm 5781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Rel 𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
25911, 257, 2583syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
260256, 259eqtr3d 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
26134ineq2d 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))))
262 fzssp1 12800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1))
263 sseqin2 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
264262, 263mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)
265264a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
266 incom 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))
267266, 132syl5eq 2843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅)
268265, 267uneq12d 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅))
269 uncom 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
270 indi 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
271269, 270eqtr4i 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
272 un0 4264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀)
273268, 271, 2723eqtr3g 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀))
274261, 273eqtrd 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀))
275274reseq2d 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
276260, 275sylan9req 2852 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
277276rneqd 5690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)))
278 df-ima 5456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))
279 df-ima 5456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))
280277, 278, 2793eqtr4g 2856 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀)))
281280xpeq1d 5472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
282281reseq1d 5733 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)))
283 relxp 5461 . . . . . . . . . . . . . . . . . . . . . . . 24 Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
284 dmxpss 5904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀))
285 imassrn 5817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈
286284, 285sstri 3898 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈
287286, 223syl5ss 3900 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀))
288 relssres 5774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∧ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
289283, 287, 288sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
290289adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
291282, 290eqtrd 2831 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
292 imassrn 5817 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
293292, 229sseqtri 3924 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)}
294 ssrin 4130 . . . . . . . . . . . . . . . . . . . . . . . . . 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, 234sseqtrid 3940 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅)
297 ss0 4272 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
298296, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
299 fnconstg 6435 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
300 fnresdisj 6337 . . . . . . . . . . . . . . . . . . . . . . . 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 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
303302adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
304291, 303uneq12d 4061 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅))
305193xpeq1i 5469 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0})
306 xpundir 5507 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
307305, 306eqtri 2819 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
308307reseq1i 5730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))
309 resundir 5749 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
310308, 309eqtr2i 2820 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))
311 un0 4264 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
312304, 310, 3113eqtr3g 2854 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
313252, 312uneq12d 4061 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
314216, 313syl5eq 2843 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
315314fveq1d 6540 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
316215, 315sylan9eqr 2853 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
317213, 316oveq12d 7034 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))
318317mpteq2dva 5055 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
319318uneq1d 4059 . . . . . . . . . . . 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 2837 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
321320uneq1d 4059 . . . . . . . . . 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 2834 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
323322csbeq1d 3815 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵)
324323eqeq2d 2805 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
325324rexbidva 3259 . . . . . 6 (𝜑 → (∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 ↔ ∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
326325ralbidv 3164 . . . . 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 230 . . . 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 6484 . . . . . . . 8 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀))
32911, 328syl 17 . . . . . . 7 (𝜑𝑈 Fn (1...𝑀))
33075, 75fnsn 6282 . . . . . . . . 9 {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)}
331 fvun2 6622 . . . . . . . . 9 ((𝑈 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
332330, 331mp3an2 1441 . . . . . . . 8 ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
333163, 332mpanr2 700 . . . . . . 7 ((𝑈 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
334329, 92, 333syl2anc 584 . . . . . 6 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
33575, 75fvsn 6806 . . . . . 6 ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)) = (𝑀 + 1)
336334, 335syl6eq 2847 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))
337170, 336jca 512 . . . 4 (𝜑 → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))
338327, 337jctird 527 . . 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 1088 . . 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 253 . 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 521 . . . . . 6 (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}))
342341, 92, 96syl2anc 584 . . . . 5 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
343342, 114mpbid 233 . . . 4 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
344 ovex 7048 . . . . 5 (0..^𝐾) ∈ V
345 ovex 7048 . . . . 5 (1...(𝑀 + 1)) ∈ V
346344, 345elmap 8285 . . . 4 ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
347343, 346sylibr 235 . . 3 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))))
348 ovex 7048 . . . . . . . 8 (1...𝑀) ∈ V
349 f1oexrnex 7488 . . . . . . . 8 ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V)
35011, 348, 349sylancl 586 . . . . . . 7 (𝜑𝑈 ∈ V)
351 snex 5223 . . . . . . 7 {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V
352 unexg 7329 . . . . . . 7 ((𝑈 ∈ V ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
353350, 351, 352sylancl 586 . . . . . 6 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
354 f1oeq1 6472 . . . . . . 7 (𝑓 = (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
355354elabg 3604 . . . . . 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 6475 . . . . . 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 584 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
359356, 358bitrd 280 . . . 4 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
360126, 359mpbird 258 . . 3 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})
361 opelxpi 5480 . . 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 584 . 2 (𝜑 → ⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}))
363340, 362jctild 526 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 207   ∧ wa 396   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081  {cab 2775  ∀wral 3105  ∃wrex 3106  Vcvv 3437  ⦋csb 3811   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4211  {csn 4472  ⟨cop 4478   class class class wbr 4962   ↦ cmpt 5041   × cxp 5441  ◡ccnv 5442  dom cdm 5443  ran crn 5444   ↾ cres 5445   “ cima 5446  Rel wrel 5448  Fun wfun 6219   Fn wfn 6220  ⟶wf 6221  –onto→wfo 6223  –1-1-onto→wf1o 6224  ‘cfv 6225  (class class class)co 7016   ∘𝑓 cof 7265   ↑𝑚 cmap 8256  0cc0 10383  1c1 10384   + caddc 10386   < clt 10521   ≤ cle 10522   − cmin 10717  ℕcn 11486  ℕ0cn0 11745  ℤcz 11829  ℤ≥cuz 12093  ...cfz 12742  ..^cfzo 12883 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-n0 11746  df-z 11830  df-uz 12094  df-fz 12743  df-fzo 12884 This theorem is referenced by:  poimirlem4  34446
 Copyright terms: Public domain W3C validator