poimirlem3 - Mathbox for Brendan Leahy

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

Theorem poimirlem3 36081

Description: Lemma for poimir 36111 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	⊢ (𝜑 → 𝑀 ∈ ℕ₀)
poimirlem4.3	⊢ (𝜑 → 𝑀 < 𝑁)
poimirlem3.4	⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾))
poimirlem3.5	⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀))

**Assertion**
Ref	Expression
poimirlem3	⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑_m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 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.

Step	Hyp	Ref	Expression
1		poimirlem3.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾))
2	1	ffnd 6669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn (1...𝑀))
3	2	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀))
4		1ex 11151	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
5		fnconstg 6730	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
6	4, 5	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
7		c0ex 11149	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
8		fnconstg 6730	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))
10	6, 9	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
11		poimirlem3.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀))
12		dff1o3 6790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun ^◡𝑈))
13	12	simprbi 497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun ^◡𝑈)
14		imain 6586	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
15	11, 13, 14	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
16		elfznn0 13534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
17	16	nn0red 12474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
18	17	ltp1d 12085	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1))
19		fzdisj 13468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
21	20	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅))
22		ima0 6029	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 “ ∅) = ∅
23	21, 22	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅)
24	15, 23	sylan9req 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅)
25		fnun 6614	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
26	10, 24, 25	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))))
27		imaundi 6102	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))
28		nn0p1nn 12452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
29		nnuz 12806	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
30	28, 29	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ (ℤ_≥‘1))
31	16, 30	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈ (ℤ_≥‘1))
32		elfzuz3 13438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑗))
33		fzsplit2 13466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑀 ∈ (ℤ_≥‘𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
34	31, 32, 33	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
35	34	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀))
36	35	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀)))
37		f1ofo 6791	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀))
38		foima 6761	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀))
39	11, 37, 38	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀))
40	36, 39	sylan9eqr 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀))
41	27, 40	eqtr3id 2790	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀))
42	41	fneq2d 6596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)))
43	26, 42	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))
44		ovexd 7392	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V)
45		inidm 4178	. . . . . . . . . . . . 13 ⊢ ((1...𝑀) ∩ (1...𝑀)) = (1...𝑀)
46		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇‘𝑛) = (𝑇‘𝑛))
47		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
48	3, 43, 44, 44, 45, 46, 47	offval 7626	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
49		poimirlem4.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
50		nn0p1nn 12452	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ)
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
52	51	nnzd 12526	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℤ)
53		uzid 12778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
54		peano2uz 12826	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
55	52, 53, 54	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑀 + 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
56		poimirlem4.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < 𝑁)
57	49	nn0zd 12525	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
58		poimir.0	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
59	58	nnzd 12526	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℤ)
60		zltp1le 12553	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
61		peano2z 12544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
62		eluz 12777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
63	61, 62	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
64	60, 63	bitr4d 281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ_≥‘(𝑀 + 1))))
65	57, 59, 64	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ_≥‘(𝑀 + 1))))
66	56, 65	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
67		fzsplit2 13466	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑀 + 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
68	55, 66, 67	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
69		fzsn 13483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 + 1) ∈ ℤ → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
70	52, 69	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
71	70	uneq1d 4122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
72	68, 71	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
73	72	xpeq1d 5662	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}))
74		xpundir 5701	. . . . . . . . . . . . . . 15 ⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
75		ovex 7390	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 + 1) ∈ V
76	75, 7	xpsn 7087	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑀 + 1)} × {0}) = {⟨(𝑀 + 1), 0⟩}
77	76	uneq1i 4119	. . . . . . . . . . . . . . 15 ⊢ (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
78	74, 77	eqtri 2764	. . . . . . . . . . . . . 14 ⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
79	73, 78	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
80	79	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
81	48, 80	uneq12d 4124	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))))
82		unass 4126	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
83	81, 82	eqtr4di 2794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
84	49	nn0red 12474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
85	84	ltp1d 12085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
86	51	nnred 12168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
87	84, 86	ltnled 11302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
88	85, 87	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
89		elfzle2 13445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀)
90	88, 89	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀))
91		disjsn 4672	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ↔ ¬ (𝑀 + 1) ∈ (1...𝑀))
92	90, 91	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)
93		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩}
94	75, 7	fsn 7081	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0} ↔ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩})
95	93, 94	mpbir 230	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}
96		fun 6704	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
97	95, 96	mpanl2 699	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
98	1, 92, 97	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
99		1z 12533	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
100		nn0uz 12805	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ₀ = (ℤ_≥‘0)
101		1m1e0 12225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 1) = 0
102	101	fveq2i 6845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
103	100, 102	eqtr4i 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
104	49, 103	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(1 − 1)))
105		fzsuc2 13499	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ (ℤ_≥‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
106	99, 104, 105	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
107	106	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
108		poimirlem4.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℕ)
109		lbfzo0 13612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^𝐾) ↔ 𝐾 ∈ ℕ)
110	108, 109	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ∈ (0..^𝐾))
111	110	snssd 4769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {0} ⊆ (0..^𝐾))
112		ssequn2 4143	. . . . . . . . . . . . . . . . . 18 ⊢ ({0} ⊆ (0..^𝐾) ↔ ((0..^𝐾) ∪ {0}) = (0..^𝐾))
113	111, 112	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾))
114	107, 113	feq23d 6663	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾)))
115	98, 114	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
116	115	ffnd 6669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
117	116	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
118		fnconstg 6730	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ V → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)))
119	4, 118	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗))
120		fnconstg 6730	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ V → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
121	7, 120	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))
122	119, 121	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
123	75, 75	f1osn 6824	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨(𝑀 + 1), (𝑀 + 1)⟩}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}
124		f1oun 6803	. . . . . . . . . . . . . . . . . . 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)}))
125	123, 124	mpanl2 699	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
126	11, 92, 92, 125	syl12anc 835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
127		dff1o3 6790	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun ^◡(𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})))
128	127	simprbi 497	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun ^◡(𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}))
129		imain 6586	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ^◡(𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
130	126, 128, 129	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
131		fzdisj 13468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
132	18, 131	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
133	132	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅))
134		ima0 6029	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅) = ∅
135	133, 134	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
136	130, 135	sylan9req 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
137		fnun 6614	. . . . . . . . . . . . . . 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)))))
138	122, 136, 137	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
139		f1ofo 6791	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}))
140		foima 6761	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)}))
141	126, 139, 140	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)}))
142	106	imaeq2d 6013	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})))
143	141, 142, 106	3eqtr4d 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1)))
144		peano2uz 12826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘𝑗) → (𝑀 + 1) ∈ (ℤ_≥‘𝑗))
145	32, 144	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ (ℤ_≥‘𝑗))
146		fzsplit2 13466	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ (𝑀 + 1) ∈ (ℤ_≥‘𝑗)) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
147	31, 145, 146	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))
148	147	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
149	143, 148	sylan9req 2797	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
150		imaundi 6102	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
151	149, 150	eqtrdi 2792	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
152	151	fneq2d 6596	. . . . . . . . . . . . . 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))))))
153	138, 152	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)))
154		ovexd 7392	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V)
155		inidm 4178	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 1)) ∩ (1...(𝑀 + 1))) = (1...(𝑀 + 1))
156		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛))
157		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
158	117, 153, 154, 154, 155, 156, 157	offval 7626	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = (𝑛 ∈ (1...(𝑀 + 1)) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))))
159		imadmrn 6023	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)})
160	75, 75	xpsn 7087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(𝑀 + 1)} × {(𝑀 + 1)}) = {⟨(𝑀 + 1), (𝑀 + 1)⟩}
161	160	imaeq1i 6010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)}))
162		dmxpid 5885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
163	162	imaeq2i 6011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
164	161, 163	eqtri 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
165		rnxpid 6125	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
166	159, 164, 165	3eqtr3ri 2773	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑀 + 1)} = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
167		eluzp1p1 12791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (ℤ_≥‘𝑗) → (𝑀 + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
168		eluzfz2 13449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
169	32, 167, 168	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
170	169	snssd 4769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)))
171		imass2 6054	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
172	170, 171	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)}) ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
173	166, 172	eqsstrid 3992	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
174	75	snid 4622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 + 1) ∈ {(𝑀 + 1)}
175		ssel 3937	. . . . . . . . . . . . . . . . 17 ⊢ ({(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → ((𝑀 + 1) ∈ {(𝑀 + 1)} → (𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
176	173, 174, 175	mpisyl 21	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
177		elun2 4137	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
178	176, 177	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))))
179		imaundir 6103	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
180	178, 179	eleqtrrdi 2849	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
181	180	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
182	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ V)
183	107	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
184		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)))
185	75, 7	fnsn 6559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)}
186		fvun2 6933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
187	185, 186	mp3an2 1449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
188	174, 187	mpanr2 702	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
189	2, 92, 188	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
190	75, 7	fvsn 7127	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)) = 0
191	189, 190	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0)
192	184, 191	sylan9eqr 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
193	192	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
194		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)))
195		fvun2 6933	. . . . . . . . . . . . . . . . . . 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)))
196	119, 121, 195	mp3an12 1451	. . . . . . . . . . . . . . . . . 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)))
197	136, 181, 196	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)))
198	7	fvconst2 7153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
199	180, 198	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
200	199	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
201	197, 200	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0)
202	194, 201	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0)
203	193, 202	oveq12d 7375	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0))
204		00id 11330	. . . . . . . . . . . . . 14 ⊢ (0 + 0) = 0
205	203, 204	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0)
206	181, 182, 183, 205	fmptapd 7117	. . . . . . . . . . . 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}))‘𝑛))))
207	2, 92	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅))
208		fvun1 6932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
209	185, 208	mp3an2 1449	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
210	209	anassrs 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
211	207, 210	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
212	211	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
213		fvres 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
214	213	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛))
215		resundir 5952	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
216		relxp 5651	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Rel ((𝑈 “ (1...𝑗)) × {1})
217		dmxpss 6123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗))
218		imassrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈 “ (1...𝑗)) ⊆ ran 𝑈
219	217, 218	sstri 3953	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ ran 𝑈
220		f1of 6784	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀))
221		frn 6675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀))
222	11, 220, 221	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑀))
223	219, 222	sstrid 3955	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀))
224		relssres 5978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Rel ((𝑈 “ (1...𝑗)) × {1}) ∧ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
225	216, 223, 224	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
226	225	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
227		imassrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
228	75	rnsnop 6176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩} = {(𝑀 + 1)}
229	227, 228	sseqtri 3980	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)}
230		ssrin 4193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
231	229, 230	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
232		incom 4161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)})
233	232, 92	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅)
234	231, 233	sseqtrid 3996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅)
235		ss0 4358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
237		fnconstg 6730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
238		fnresdisj 6621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅))
239	4, 237, 238	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
240	236, 239	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
241	240	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
242	226, 241	uneq12d 4124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅))
243		imaundir 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
244	243	xpeq1i 5659	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1})
245		xpundir 5701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
246	244, 245	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
247	246	reseq1i 5933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀))
248		resundir 5952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)))
249	247, 248	eqtr2i 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀))
250		un0 4350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1})
251	242, 249, 250	3eqtr3g 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
252		f1odm 6788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀))
253	11, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → dom 𝑈 = (1...𝑀))
254	253	ineq2d 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))
255	254	reseq2d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))))
256		f1orel 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈)
257		resindm 5986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Rel 𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
258	11, 256, 257	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
259	255, 258	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
260	34	ineq2d 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))))
261		fzssp1 13484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1))
262		sseqin2 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
263	261, 262	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
265		incom 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))
266	265, 132	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅)
267	264, 266	uneq12d 4124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅))
268		uncom 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
269		indi 4233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
270	268, 269	eqtr4i 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
271		un0 4350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀)
272	267, 270, 271	3eqtr3g 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀))
273	260, 272	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀))
274	273	reseq2d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
275	259, 274	sylan9req 2797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
276	275	rneqd 5893	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)))
277		df-ima 5646	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))
278		df-ima 5646	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))
279	276, 277, 278	3eqtr4g 2801	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀)))
280	279	xpeq1d 5662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
281	280	reseq1d 5936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)))
282		relxp 5651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
283		dmxpss 6123	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀))
284		imassrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈
285	283, 284	sstri 3953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈
286	285, 222	sstrid 3955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀))
287		relssres 5978	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∧ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
288	282, 286, 287	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
289	288	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
290	281, 289	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
291		imassrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
292	291, 228	sseqtri 3980	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)}
293		ssrin 4193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)))
294	292, 293	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))
295	294, 233	sseqtrid 3996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅)
296		ss0 4358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
297	295, 296	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
298		fnconstg 6730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
299		fnresdisj 6621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅))
300	7, 298, 299	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
301	297, 300	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
302	301	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
303	290, 302	uneq12d 4124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅))
304	179	xpeq1i 5659	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0})
305		xpundir 5701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
306	304, 305	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
307	306	reseq1i 5933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))
308		resundir 5952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
309	307, 308	eqtr2i 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))
310		un0 4350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
311	303, 309, 310	3eqtr3g 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
312	251, 311	uneq12d 4124	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
313	215, 312	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
314	313	fveq1d 6844	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
315	214, 314	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
316	212, 315	oveq12d 7375	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))
317	316	mpteq2dva 5205	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
318	317	uneq1d 4122	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
319	158, 206, 318	3eqtr2d 2782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
320	319	uneq1d 4122	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
321	83, 320	eqtr4d 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
322	321	csbeq1d 3859	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)
323	322	eqeq2d 2747	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ 𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵))
324	323	rexbidva 3173	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ ∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵))
325	324	ralbidv 3174	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵))
326	325	biimpd 228	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵))
327		f1ofn 6785	. . . . . . . 8 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀))
328	11, 327	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 Fn (1...𝑀))
329	75, 75	fnsn 6559	. . . . . . . . 9 ⊢ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)}
330		fvun2 6933	. . . . . . . . 9 ⊢ ((𝑈 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
331	329, 330	mp3an2 1449	. . . . . . . 8 ⊢ ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
332	174, 331	mpanr2 702	. . . . . . 7 ⊢ ((𝑈 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
333	328, 92, 332	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
334	75, 75	fvsn 7127	. . . . . 6 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)) = (𝑀 + 1)
335	333, 334	eqtrdi 2792	. . . . 5 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))
336	191, 335	jca 512	. . . 4 ⊢ (𝜑 → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))
337	326, 336	jctird 527	. . 3 ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))
338		3anass 1095	. . 3 ⊢ ((∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))))
339	337, 338	syl6ibr 251	. 2 ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))))
340	1, 95	jctir 521	. . . . . 6 ⊢ (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}))
341	340, 92, 96	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
342	341, 114	mpbid 231	. . . 4 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
343		ovex 7390	. . . . 5 ⊢ (0..^𝐾) ∈ V
344		ovex 7390	. . . . 5 ⊢ (1...(𝑀 + 1)) ∈ V
345	343, 344	elmap 8809	. . . 4 ⊢ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑_m (1...(𝑀 + 1))) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
346	342, 345	sylibr 233	. . 3 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑_m (1...(𝑀 + 1))))
347		ovex 7390	. . . . . . . 8 ⊢ (1...𝑀) ∈ V
348		f1oexrnex 7864	. . . . . . . 8 ⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V)
349	11, 347, 348	sylancl 586	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ V)
350		snex 5388	. . . . . . 7 ⊢ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V
351		unexg 7683	. . . . . . 7 ⊢ ((𝑈 ∈ V ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
352	349, 350, 351	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
353		f1oeq1 6772	. . . . . . 7 ⊢ (𝑓 = (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
354	353	elabg 3628	. . . . . 6 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
355	352, 354	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
356		f1oeq23 6775	. . . . . 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)})))
357	106, 106, 356	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
358	355, 357	bitrd 278	. . . 4 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
359	126, 358	mpbird 256	. . 3 ⊢ (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})
360	346, 359	opelxpd 5671	. 2 ⊢ (𝜑 → ⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑_m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}))
361	339, 360	jctild 526	1 ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑_m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 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 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {cab 2713 ∀wral 3064 ∃wrex 3073 Vcvv 3445 ⦋csb 3855 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 {csn 4586 ⟨cop 4592 class class class wbr 5105 ↦ cmpt 5188 × cxp 5631 ^◡ccnv 5632 dom cdm 5633 ran crn 5634 ↾ cres 5635 “ cima 5636 Rel wrel 5638 Fun wfun 6490 Fn wfn 6491 ⟶wf 6492 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 ∘_f cof 7615 ↑_m cmap 8765 0cc0 11051 1c1 11052 + caddc 11054 < clt 11189 ≤ cle 11190 − cmin 11385 ℕcn 12153 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ...cfz 13424 ..^cfzo 13567

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-n0 12414 df-z 12500 df-uz 12764 df-fz 13425 df-fzo 13568

This theorem is referenced by: poimirlem4 36082

W3C validator