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 33542
Description: Lemma for poimir 33572 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..^𝐾))
2 ffn 6083 . . . . . . . . . . . . . . 15 (𝑇:(1...𝑀)⟶(0..^𝐾) → 𝑇 Fn (1...𝑀))
31, 2syl 17 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑀))
43adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀))
5 1ex 10073 . . . . . . . . . . . . . . . . 17 1 ∈ V
6 fnconstg 6131 . . . . . . . . . . . . . . . . 17 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
75, 6ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
8 c0ex 10072 . . . . . . . . . . . . . . . . 17 0 ∈ V
9 fnconstg 6131 . . . . . . . . . . . . . . . . 17 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
108, 9ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))
117, 10pm3.2i 470 . . . . . . . . . . . . . . 15 (((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
12 poimirlem3.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑈:(1...𝑀)–1-1-onto→(1...𝑀))
13 dff1o3 6181 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun 𝑈))
1413simprbi 479 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun 𝑈)
15 imain 6012 . . . . . . . . . . . . . . . . 17 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
1612, 14, 153syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
17 elfznn0 12471 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
1817nn0red 11390 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
1918ltp1d 10992 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1))
20 fzdisj 12406 . . . . . . . . . . . . . . . . . . 19 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
2119, 20syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
2221imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅))
23 ima0 5516 . . . . . . . . . . . . . . . . 17 (𝑈 “ ∅) = ∅
2422, 23syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅)
2516, 24sylan9req 2706 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅)
26 fnun 6035 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
2711, 25, 26sylancr 696 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
28 imaundi 5580 . . . . . . . . . . . . . . . 16 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))
29 nn0p1nn 11370 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
30 nnuz 11761 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
3129, 30syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ (ℤ‘1))
3217, 31syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈ (ℤ‘1))
33 elfzuz3 12377 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ𝑗))
34 fzsplit2 12404 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑀 ∈ (ℤ𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
3532, 33, 34syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
3635eqcomd 2657 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀))
3736imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀)))
38 f1ofo 6182 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀))
39 foima 6158 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀))
4012, 38, 393syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀))
4137, 40sylan9eqr 2707 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀))
4228, 41syl5eqr 2699 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀))
4342fneq2d 6020 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)))
4427, 43mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))
45 ovexd 6720 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V)
46 inidm 3855 . . . . . . . . . . . . 13 ((1...𝑀) ∩ (1...𝑀)) = (1...𝑀)
47 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇𝑛) = (𝑇𝑛))
48 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
494, 44, 45, 45, 46, 47, 48offval 6946 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
50 poimirlem4.2 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℕ0)
51 nn0p1nn 11370 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
5250, 51syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 + 1) ∈ ℕ)
5352nnzd 11519 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℤ)
54 uzid 11740 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ (ℤ‘(𝑀 + 1)))
55 peano2uz 11779 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ (ℤ‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
5653, 54, 553syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
57 poimirlem4.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 < 𝑁)
5850nn0zd 11518 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
59 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
6059nnzd 11519 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
61 zltp1le 11465 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
62 peano2z 11456 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
63 eluz 11739 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
6462, 63sylan 487 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
6561, 64bitr4d 271 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁𝑁 ∈ (ℤ‘(𝑀 + 1))))
6658, 60, 65syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 < 𝑁𝑁 ∈ (ℤ‘(𝑀 + 1))))
6757, 66mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
68 fzsplit2 12404 . . . . . . . . . . . . . . . . 17 ((((𝑀 + 1) + 1) ∈ (ℤ‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
6956, 67, 68syl2anc 694 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
70 fzsn 12421 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ ℤ → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
7153, 70syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
7271uneq1d 3799 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
7369, 72eqtrd 2685 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
7473xpeq1d 5172 . . . . . . . . . . . . . 14 (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}))
75 xpundir 5206 . . . . . . . . . . . . . . 15 (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
76 ovex 6718 . . . . . . . . . . . . . . . . 17 (𝑀 + 1) ∈ V
7776, 8xpsn 6447 . . . . . . . . . . . . . . . 16 ({(𝑀 + 1)} × {0}) = {⟨(𝑀 + 1), 0⟩}
7877uneq1i 3796 . . . . . . . . . . . . . . 15 (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
7975, 78eqtri 2673 . . . . . . . . . . . . . 14 (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
8074, 79syl6eq 2701 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8180adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8249, 81uneq12d 3801 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))))
83 unass 3803 . . . . . . . . . . 11 (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8482, 83syl6eqr 2703 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
8550nn0red 11390 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ ℝ)
8685ltp1d 10992 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 < (𝑀 + 1))
8752nnred 11073 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 + 1) ∈ ℝ)
8885, 87ltnled 10222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
8986, 88mpbid 222 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
90 elfzle2 12383 . . . . . . . . . . . . . . . . . . 19 ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀)
9189, 90nsyl 135 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀))
92 disjsn 4278 . . . . . . . . . . . . . . . . . 18 (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ↔ ¬ (𝑀 + 1) ∈ (1...𝑀))
9391, 92sylibr 224 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)
94 eqid 2651 . . . . . . . . . . . . . . . . . . 19 {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩}
9576, 8fsn 6442 . . . . . . . . . . . . . . . . . . 19 ({⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0} ↔ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩})
9694, 95mpbir 221 . . . . . . . . . . . . . . . . . 18 {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}
97 fun 6104 . . . . . . . . . . . . . . . . . 18 (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
9896, 97mpanl2 717 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
991, 93, 98syl2anc 694 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
100 1z 11445 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℤ
101 nn0uz 11760 . . . . . . . . . . . . . . . . . . . . 21 0 = (ℤ‘0)
102 1m1e0 11127 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 1) = 0
103102fveq2i 6232 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘(1 − 1)) = (ℤ‘0)
104101, 103eqtr4i 2676 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘(1 − 1))
10550, 104syl6eleq 2740 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (ℤ‘(1 − 1)))
106 fzsuc2 12436 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℤ ∧ 𝑀 ∈ (ℤ‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
107100, 105, 106sylancr 696 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
108107eqcomd 2657 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
109 poimirlem4.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℕ)
110 lbfzo0 12547 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ (0..^𝐾) ↔ 𝐾 ∈ ℕ)
111109, 110sylibr 224 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ∈ (0..^𝐾))
112111snssd 4372 . . . . . . . . . . . . . . . . . 18 (𝜑 → {0} ⊆ (0..^𝐾))
113 ssequn2 3819 . . . . . . . . . . . . . . . . . 18 ({0} ⊆ (0..^𝐾) ↔ ((0..^𝐾) ∪ {0}) = (0..^𝐾))
114112, 113sylib 208 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾))
115108, 114feq23d 6078 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾)))
11699, 115mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
117 ffn 6083 . . . . . . . . . . . . . . 15 ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
118116, 117syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
119118adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
120 fnconstg 6131 . . . . . . . . . . . . . . . . 17 (1 ∈ V → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)))
1215, 120ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗))
122 fnconstg 6131 . . . . . . . . . . . . . . . . 17 (0 ∈ V → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
1238, 122ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))
124121, 123pm3.2i 470 . . . . . . . . . . . . . . 15 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
12576, 76f1osn 6214 . . . . . . . . . . . . . . . . . . 19 {⟨(𝑀 + 1), (𝑀 + 1)⟩}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}
126 f1oun 6194 . . . . . . . . . . . . . . . . . . 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)}))
127125, 126mpanl2 717 . . . . . . . . . . . . . . . . . 18 ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
12812, 93, 93, 127syl12anc 1364 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
129 dff1o3 6181 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})))
130129simprbi 479 . . . . . . . . . . . . . . . . 17 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}))
131 imain 6012 . . . . . . . . . . . . . . . . 17 (Fun (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
132128, 130, 1313syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
133 fzdisj 12406 . . . . . . . . . . . . . . . . . . 19 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
13419, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
135134imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅))
136 ima0 5516 . . . . . . . . . . . . . . . . 17 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅) = ∅
137135, 136syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
138132, 137sylan9req 2706 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
139 fnun 6035 . . . . . . . . . . . . . . 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)))))
140124, 138, 139sylancr 696 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
141 f1ofo 6182 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}))
142 foima 6158 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)}))
143128, 141, 1423syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)}))
144107imaeq2d 5501 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})))
145143, 144, 1073eqtr4d 2695 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1)))
146 peano2uz 11779 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ𝑗) → (𝑀 + 1) ∈ (ℤ𝑗))
14733, 146syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ (ℤ𝑗))
148 fzsplit2 12404 . . . . . . . . . . . . . . . . . . 19 (((𝑗 + 1) ∈ (ℤ‘1) ∧ (𝑀 + 1) ∈ (ℤ𝑗)) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
14932, 147, 148syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
150149imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
151145, 150sylan9req 2706 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
152 imaundi 5580 . . . . . . . . . . . . . . . 16 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
153151, 152syl6eq 2701 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
154153fneq2d 6020 . . . . . . . . . . . . . 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))))))
155140, 154mpbird 247 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)))
156 ovexd 6720 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V)
157 inidm 3855 . . . . . . . . . . . . 13 ((1...(𝑀 + 1)) ∩ (1...(𝑀 + 1))) = (1...(𝑀 + 1))
158 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛))
159 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
160119, 155, 156, 156, 157, 158, 159offval 6946 . . . . . . . . . . . 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}))‘𝑛))))
161 ovexd 6720 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ V)
1628a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ V)
163108adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
164 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)))
16576snid 4241 . . . . . . . . . . . . . . . . . . . 20 (𝑀 + 1) ∈ {(𝑀 + 1)}
16676, 8fnsn 5984 . . . . . . . . . . . . . . . . . . . . 21 {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)}
167 fvun2 6309 . . . . . . . . . . . . . . . . . . . . 21 ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
168166, 167mp3an2 1452 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
169165, 168mpanr2 720 . . . . . . . . . . . . . . . . . . 19 ((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
1703, 93, 169syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
17176, 8fvsn 6487 . . . . . . . . . . . . . . . . . 18 ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)) = 0
172170, 171syl6eq 2701 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0)
173164, 172sylan9eqr 2707 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
174173adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
175 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)))
176 imadmrn 5511 . . . . . . . . . . . . . . . . . . . . . . . 24 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)})
17776, 76xpsn 6447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝑀 + 1)} × {(𝑀 + 1)}) = {⟨(𝑀 + 1), (𝑀 + 1)⟩}
178177imaeq1i 5498 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)}))
179 dmxpid 5377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
180179imaeq2i 5499 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
181178, 180eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . 24 (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
182 rnxpid 5602 . . . . . . . . . . . . . . . . . . . . . . . 24 ran ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
183176, 181, 1823eqtr3ri 2682 . . . . . . . . . . . . . . . . . . . . . . 23 {(𝑀 + 1)} = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
184 eluzp1p1 11751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ (ℤ𝑗) → (𝑀 + 1) ∈ (ℤ‘(𝑗 + 1)))
185 eluzfz2 12387 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 + 1) ∈ (ℤ‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
18633, 184, 1853syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
187186snssd 4372 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)))
188 imass2 5536 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
189187, 188syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (0...𝑀) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
190183, 189syl5eqss 3682 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
191 ssel 3630 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → ((𝑀 + 1) ∈ {(𝑀 + 1)} → (𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
192190, 165, 191mpisyl 21 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
193 elun2 3814 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
194192, 193syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
195 imaundir 5581 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
196194, 195syl6eleqr 2741 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
197196adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
198 fvun2 6309 . . . . . . . . . . . . . . . . . . 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)))
199121, 123, 198mp3an12 1454 . . . . . . . . . . . . . . . . . 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)))
200138, 197, 199syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)))
2018fvconst2 6510 . . . . . . . . . . . . . . . . . . 19 ((𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
202196, 201syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
203202adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
204200, 203eqtrd 2685 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0)
205175, 204sylan9eqr 2707 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0)
206174, 205oveq12d 6708 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0))
207 00id 10249 . . . . . . . . . . . . . 14 (0 + 0) = 0
208206, 207syl6eq 2701 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0)
209161, 162, 163, 208fmptapd 6478 . . . . . . . . . . . 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}))‘𝑛))))
2103, 93jca 553 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅))
211 fvun1 6308 . . . . . . . . . . . . . . . . . . 19 ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
212166, 211mp3an2 1452 . . . . . . . . . . . . . . . . . 18 ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
213212anassrs 681 . . . . . . . . . . . . . . . . 17 (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
214210, 213sylan 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
215214adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇𝑛))
216 fvres 6245 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
217216eqcomd 2657 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛))
218 resundir 5446 . . . . . . . . . . . . . . . . . 18 (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
219 relxp 5160 . . . . . . . . . . . . . . . . . . . . . . 23 Rel ((𝑈 “ (1...𝑗)) × {1})
220 dmxpss 5600 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗))
221 imassrn 5512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ (1...𝑗)) ⊆ ran 𝑈
222220, 221sstri 3645 . . . . . . . . . . . . . . . . . . . . . . . 24 dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ ran 𝑈
223 f1of 6175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀))
224 frn 6091 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀))
22512, 223, 2243syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ran 𝑈 ⊆ (1...𝑀))
226222, 225syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀))
227 relssres 5472 . . . . . . . . . . . . . . . . . . . . . . 23 ((Rel ((𝑈 “ (1...𝑗)) × {1}) ∧ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
228219, 226, 227sylancr 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
229228adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
230 imassrn 5512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
23176rnsnop 5653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ran {⟨(𝑀 + 1), (𝑀 + 1)⟩} = {(𝑀 + 1)}
232230, 231sseqtri 3670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)}
233 ssrin 3871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
234232, 233ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
235 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)})
236235, 93syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅)
237234, 236syl5sseq 3686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅)
238 ss0 4007 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
239237, 238syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
240 fnconstg 6131 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
241 fnresdisj 6039 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅))
2425, 240, 241mp2b 10 . . . . . . . . . . . . . . . . . . . . . . 23 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
243239, 242sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
244243adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
245229, 244uneq12d 3801 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅))
246 imaundir 5581 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
247246xpeq1i 5169 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1})
248 xpundir 5206 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
249247, 248eqtri 2673 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
250249reseq1i 5424 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀))
251 resundir 5446 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)))
252250, 251eqtr2i 2674 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀))
253 un0 4000 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1})
254245, 252, 2533eqtr3g 2708 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
255 f1odm 6179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀))
25612, 255syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → dom 𝑈 = (1...𝑀))
257256ineq2d 3847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))
258257reseq2d 5428 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))))
259 f1orel 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈)
260 resindm 5479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Rel 𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
26112, 259, 2603syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
262258, 261eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
26335ineq2d 3847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))))
264 fzssp1 12422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1))
265 sseqin2 3850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
266264, 265mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)
267266a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
268 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))
269268, 134syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅)
270267, 269uneq12d 3801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅))
271 uncom 3790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
272 indi 3906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
273271, 272eqtr4i 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
274 un0 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀)
275270, 273, 2743eqtr3g 2708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀))
276263, 275eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀))
277276reseq2d 5428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
278262, 277sylan9req 2706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
279278rneqd 5385 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)))
280 df-ima 5156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))
281 df-ima 5156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))
282279, 280, 2813eqtr4g 2710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀)))
283282xpeq1d 5172 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
284283reseq1d 5427 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)))
285 relxp 5160 . . . . . . . . . . . . . . . . . . . . . . . 24 Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
286 dmxpss 5600 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀))
287 imassrn 5512 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈
288286, 287sstri 3645 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈
289288, 225syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀))
290 relssres 5472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∧ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
291285, 289, 290sylancr 696 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
292291adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
293284, 292eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
294 imassrn 5512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
295294, 231sseqtri 3670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)}
296 ssrin 3871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
297295, 296ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
298297, 236syl5sseq 3686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅)
299 ss0 4007 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
300298, 299syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
301 fnconstg 6131 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
302 fnresdisj 6039 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅))
3038, 301, 302mp2b 10 . . . . . . . . . . . . . . . . . . . . . . 23 ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
304300, 303sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
305304adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
306293, 305uneq12d 3801 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅))
307195xpeq1i 5169 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0})
308 xpundir 5206 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
309307, 308eqtri 2673 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
310309reseq1i 5424 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))
311 resundir 5446 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
312310, 311eqtr2i 2674 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))
313 un0 4000 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
314306, 312, 3133eqtr3g 2708 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
315254, 314uneq12d 3801 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
316218, 315syl5eq 2697 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
317316fveq1d 6231 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
318217, 317sylan9eqr 2707 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
319215, 318oveq12d 6708 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))
320319mpteq2dva 4777 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
321320uneq1d 3799 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
322160, 209, 3213eqtr2d 2691 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
323322uneq1d 3799 . . . . . . . . . 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})))
32484, 323eqtr4d 2688 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
325324csbeq1d 3573 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵)
326325eqeq2d 2661 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
327326rexbidva 3078 . . . . . 6 (𝜑 → (∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 ↔ ∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵))
328327ralbidv 3015 . . . . 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})) / 𝑝𝐵))
329328biimpd 219 . . . 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})) / 𝑝𝐵))
330 f1ofn 6176 . . . . . . . 8 (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀))
33112, 330syl 17 . . . . . . 7 (𝜑𝑈 Fn (1...𝑀))
33276, 76fnsn 5984 . . . . . . . . 9 {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)}
333 fvun2 6309 . . . . . . . . 9 ((𝑈 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
334332, 333mp3an2 1452 . . . . . . . 8 ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
335165, 334mpanr2 720 . . . . . . 7 ((𝑈 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
336331, 93, 335syl2anc 694 . . . . . 6 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
33776, 76fvsn 6487 . . . . . 6 ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)) = (𝑀 + 1)
338336, 337syl6eq 2701 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))
339172, 338jca 553 . . . 4 (𝜑 → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))
340329, 339jctird 566 . . 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)))))
341 3anass 1059 . . 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))))
342340, 341syl6ibr 242 . 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))))
3431, 96jctir 560 . . . . . 6 (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}))
344343, 93, 97syl2anc 694 . . . . 5 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
345344, 115mpbid 222 . . . 4 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
346 ovex 6718 . . . . 5 (0..^𝐾) ∈ V
347 ovex 6718 . . . . 5 (1...(𝑀 + 1)) ∈ V
348346, 347elmap 7928 . . . 4 ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
349345, 348sylibr 224 . . 3 (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))))
350 ovex 6718 . . . . . . . 8 (1...𝑀) ∈ V
351 f1oexrnex 7157 . . . . . . . 8 ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V)
35212, 350, 351sylancl 695 . . . . . . 7 (𝜑𝑈 ∈ V)
353 snex 4938 . . . . . . 7 {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V
354 unexg 7001 . . . . . . 7 ((𝑈 ∈ V ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
355352, 353, 354sylancl 695 . . . . . 6 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
356 f1oeq1 6165 . . . . . . 7 (𝑓 = (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
357356elabg 3383 . . . . . 6 ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
358355, 357syl 17 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
359 f1oeq23 6168 . . . . . 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)})))
360107, 107, 359syl2anc 694 . . . . 5 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
361358, 360bitrd 268 . . . 4 (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
362128, 361mpbird 247 . . 3 (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})
363 opelxpi 5182 . . 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))}))
364349, 362, 363syl2anc 694 . 2 (𝜑 → ⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}))
365342, 364jctild 565 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 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  Vcvv 3231  csb 3566  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210  cop 4216   class class class wbr 4685  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Rel wrel 5148  Fun wfun 5920   Fn wfn 5921  wf 5922  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  𝑓 cof 6937  𝑚 cmap 7899  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  cn 11058  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  ..^cfzo 12504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505
This theorem is referenced by:  poimirlem4  33543
  Copyright terms: Public domain W3C validator