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 37630

Description: Lemma for poimir 37660 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 6737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn (1...𝑀))
3	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀))
4		1ex 11257	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
5		fnconstg 6796	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
6	4, 5	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
7		c0ex 11255	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
8		fnconstg 6796	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))
10	6, 9	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)))
11		poimirlem3.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀))
12		dff1o3 6854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun ^◡𝑈))
13	12	simprbi 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun ^◡𝑈)
14		imain 6651	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
15	11, 13, 14	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))))
16		elfznn0 13660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
17	16	nn0red 12588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
18	17	ltp1d 12198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1))
19		fzdisj 13591	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅)
21	20	imaeq2d 6078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅))
22		ima0 6095	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 “ ∅) = ∅
23	21, 22	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅)
24	15, 23	sylan9req 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅)
25		fnun 6682	. . . . . . . . . . . . . . 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 6169	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))
28		nn0p1nn 12565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
29		nnuz 12921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
30	28, 29	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ (ℤ_≥‘1))
31	16, 30	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈ (ℤ_≥‘1))
32		elfzuz3 13561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑗))
33		fzsplit2 13589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑀 ∈ (ℤ_≥‘𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
34	31, 32, 33	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
35	34	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀))
36	35	imaeq2d 6078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀)))
37		f1ofo 6855	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀))
38		foima 6825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀))
39	11, 37, 38	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀))
40	36, 39	sylan9eqr 2799	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀))
41	27, 40	eqtr3id 2791	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀))
42	41	fneq2d 6662	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)))
43	26, 42	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))
44		ovexd 7466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V)
45		inidm 4227	. . . . . . . . . . . . 13 ⊢ ((1...𝑀) ∩ (1...𝑀)) = (1...𝑀)
46		eqidd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇‘𝑛) = (𝑇‘𝑛))
47		eqidd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
48	3, 43, 44, 44, 45, 46, 47	offval 7706	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
49		poimirlem4.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
50		nn0p1nn 12565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ)
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
52	51	nnzd 12640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℤ)
53		uzid 12893	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
54		peano2uz 12943	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
55	52, 53, 54	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑀 + 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
56		poimirlem4.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < 𝑁)
57	49	nn0zd 12639	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
58		poimir.0	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
59	58	nnzd 12640	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℤ)
60		zltp1le 12667	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
61		peano2z 12658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
62		eluz 12892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
63	61, 62	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁))
64	60, 63	bitr4d 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ_≥‘(𝑀 + 1))))
65	57, 59, 64	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ_≥‘(𝑀 + 1))))
66	56, 65	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
67		fzsplit2 13589	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑀 + 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
68	55, 66, 67	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
69		fzsn 13606	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 + 1) ∈ ℤ → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
70	52, 69	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)})
71	70	uneq1d 4167	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
72	68, 71	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)))
73	72	xpeq1d 5714	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}))
74		xpundir 5755	. . . . . . . . . . . . . . 15 ⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
75		ovex 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 + 1) ∈ V
76	75, 7	xpsn 7161	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑀 + 1)} × {0}) = {⟨(𝑀 + 1), 0⟩}
77	76	uneq1i 4164	. . . . . . . . . . . . . . 15 ⊢ (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
78	74, 77	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))
79	73, 78	eqtrdi 2793	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
80	79	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
81	48, 80	uneq12d 4169	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({⟨(𝑀 + 1), 0⟩} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))))
82		unass 4172	. . . . . . . . . . 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 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))
84	49	nn0red 12588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
85	84	ltp1d 12198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
86	51	nnred 12281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
87	84, 86	ltnled 11408	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
88	85, 87	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
89		elfzle2 13568	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀)
90	88, 89	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀))
91		disjsn 4711	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ↔ ¬ (𝑀 + 1) ∈ (1...𝑀))
92	90, 91	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)
93		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩}
94	75, 7	fsn 7155	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0} ↔ {⟨(𝑀 + 1), 0⟩} = {⟨(𝑀 + 1), 0⟩})
95	93, 94	mpbir 231	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}
96		fun 6770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
97	95, 96	mpanl2 701	. . . . . . . . . . . . . . . . 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 12647	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
100		nn0uz 12920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ₀ = (ℤ_≥‘0)
101		1m1e0 12338	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 1) = 0
102	101	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
103	100, 102	eqtr4i 2768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
104	49, 103	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(1 − 1)))
105		fzsuc2 13622	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ (ℤ_≥‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
106	99, 104, 105	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
107	106	eqcomd 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
108		poimirlem4.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℕ)
109		lbfzo0 13739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^𝐾) ↔ 𝐾 ∈ ℕ)
110	108, 109	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ∈ (0..^𝐾))
111	110	snssd 4809	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {0} ⊆ (0..^𝐾))
112		ssequn2 4189	. . . . . . . . . . . . . . . . . 18 ⊢ ({0} ⊆ (0..^𝐾) ↔ ((0..^𝐾) ∪ {0}) = (0..^𝐾))
113	111, 112	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾))
114	107, 113	feq23d 6731	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾)))
115	98, 114	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
116	115	ffnd 6737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
117	116	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) Fn (1...(𝑀 + 1)))
118		fnconstg 6796	. . . . . . . . . . . . . . . . 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 6796	. . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∧ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
123	75, 75	f1osn 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨(𝑀 + 1), (𝑀 + 1)⟩}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}
124		f1oun 6867	. . . . . . . . . . . . . . . . . . 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 701	. . . . . . . . . . . . . . . . . 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 837	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))
127		dff1o3 6854	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun ^◡(𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})))
128	127	simprbi 496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun ^◡(𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}))
129		imain 6651	. . . . . . . . . . . . . . . . 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 13591	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
132	18, 131	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅)
133	132	imaeq2d 6078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅))
134		ima0 6095	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ∅) = ∅
135	133, 134	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
136	130, 135	sylan9req 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∩ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅)
137		fnun 6682	. . . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}))
140		foima 6825	. . . . . . . . . . . . . . . . . . 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 6078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑀) ∪ {(𝑀 + 1)})))
143	141, 142, 106	3eqtr4d 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1)))
144		peano2uz 12943	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘𝑗) → (𝑀 + 1) ∈ (ℤ_≥‘𝑗))
145	32, 144	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ (ℤ_≥‘𝑗))
146		fzsplit2 13589	. . . . . . . . . . . . . . . . . . 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 6078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
149	143, 148	sylan9req 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))))
150		imaundi 6169	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
151	149, 150	eqtrdi 2793	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) ∪ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1)))))
152	151	fneq2d 6662	. . . . . . . . . . . . . 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 257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)))
154		ovexd 7466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V)
155		inidm 4227	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 1)) ∩ (1...(𝑀 + 1))) = (1...(𝑀 + 1))
156		eqidd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛))
157		eqidd 2738	. . . . . . . . . . . . 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 7706	. . . . . . . . . . . 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 6088	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)})
160	75, 75	xpsn 7161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(𝑀 + 1)} × {(𝑀 + 1)}) = {⟨(𝑀 + 1), (𝑀 + 1)⟩}
161	160	imaeq1i 6075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)}))
162		dmxpid 5941	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
163	162	imaeq2i 6076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
164	161, 163	eqtri 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
165		rnxpid 6193	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)}
166	159, 164, 165	3eqtr3ri 2774	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑀 + 1)} = ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ {(𝑀 + 1)})
167		eluzp1p1 12906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (ℤ_≥‘𝑗) → (𝑀 + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
168		eluzfz2 13572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
169	32, 167, 168	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1)))
170	169	snssd 4809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)))
171		imass2 6120	. . . . . . . . . . . . . . . . . . 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 4022	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
174	75	snid 4662	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 + 1) ∈ {(𝑀 + 1)}
175		ssel 3977	. . . . . . . . . . . . . . . . 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 4183	. . . . . . . . . . . . . . . 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 6170	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
180	178, 179	eleqtrrdi 2852	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
181	180	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))))
182	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ V)
183	107	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1)))
184		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)))
185	75, 7	fnsn 6624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)}
186		fvun2 7001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
187	185, 186	mp3an2 1451	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)))
188	174, 187	mpanr2 704	. . . . . . . . . . . . . . . . . . 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 7201	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨(𝑀 + 1), 0⟩}‘(𝑀 + 1)) = 0
191	189, 190	eqtrdi 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0)
192	184, 191	sylan9eqr 2799	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
193	192	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = 0)
194		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)))
195		fvun2 7001	. . . . . . . . . . . . . . . . . . 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 1453	. . . . . . . . . . . . . . . . . 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 7224	. . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0)
201	197, 200	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0)
202	194, 201	sylan9eqr 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0)
203	193, 202	oveq12d 7449	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0))
204		00id 11436	. . . . . . . . . . . . . 14 ⊢ (0 + 0) = 0
205	203, 204	eqtrdi 2793	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0)
206	181, 182, 183, 205	fmptapd 7191	. . . . . . . . . . . 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 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅))
208		fvun1 7000	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), 0⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
209	185, 208	mp3an2 1451	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
210	209	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
211	207, 210	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
212	211	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) = (𝑇‘𝑛))
213		fvres 6925	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))
214	213	eqcomd 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛))
215		resundir 6012	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
216		relxp 5703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Rel ((𝑈 “ (1...𝑗)) × {1})
217		dmxpss 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗))
218		imassrn 6089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈 “ (1...𝑗)) ⊆ ran 𝑈
219	217, 218	sstri 3993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ ran 𝑈
220		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀))
221		frn 6743	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀))
222	11, 220, 221	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑀))
223	219, 222	sstrid 3995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀))
224		relssres 6040	. . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
227		imassrn 6089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
228	75	rnsnop 6244	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩} = {(𝑀 + 1)}
229	227, 228	sseqtri 4032	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ⊆ {(𝑀 + 1)}
230		ssrin 4242	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4209	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)})
233	232, 92	eqtrid 2789	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅)
234	231, 233	sseqtrid 4026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅)
235		ss0 4402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) ∩ (1...𝑀)) = ∅)
237		fnconstg 6796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
238		fnresdisj 6688	. . . . . . . . . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
241	240	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)
242	226, 241	uneq12d 4169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅))
243		imaundir 6170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)))
244	243	xpeq1i 5711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1})
245		xpundir 5755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 “ (1...𝑗)) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
246	244, 245	eqtri 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}))
247	246	reseq1i 5993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀))
248		resundir 6012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀)))
249	247, 248	eqtr2i 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀))
250		un0 4394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1})
251	242, 249, 250	3eqtr3g 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1}))
252		f1odm 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀))
253	11, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → dom 𝑈 = (1...𝑀))
254	253	ineq2d 4220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))
255	254	reseq2d 5997	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))))
256		f1orel 6851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈)
257		resindm 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Rel 𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
258	11, 256, 257	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
259	255, 258	eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))))
260	34	ineq2d 4220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))))
261		fzssp1 13607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1))
262		sseqin2 4223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
263	261, 262	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀))
265		incom 4209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))
266	265, 132	eqtrid 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅)
267	264, 266	uneq12d 4169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅))
268		uncom 4158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
269		indi 4284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)))
270	268, 269	eqtr4i 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))
271		un0 4394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀)
272	267, 270, 271	3eqtr3g 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀))
273	260, 272	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀))
274	273	reseq2d 5997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
275	259, 274	sylan9req 2798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀)))
276	275	rneqd 5949	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)))
277		df-ima 5698	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))
278		df-ima 5698	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))
279	276, 277, 278	3eqtr4g 2802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀)))
280	279	xpeq1d 5714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
281	280	reseq1d 5996	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)))
282		relxp 5703	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Rel ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
283		dmxpss 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀))
284		imassrn 6089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈
285	283, 284	sstri 3993	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈
286	285, 222	sstrid 3995	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀))
287		relssres 6040	. . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
290	281, 289	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
291		imassrn 6089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ ran {⟨(𝑀 + 1), (𝑀 + 1)⟩}
292	291, 228	sseqtri 4032	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)}
293		ssrin 4242	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅)
296		ss0 4402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
297	295, 296	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅)
298		fnconstg 6796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 ∈ V → (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))))
299		fnresdisj 6688	. . . . . . . . . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
302	301	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)
303	290, 302	uneq12d 4169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅))
304	179	xpeq1i 5711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0})
305		xpundir 5755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
306	304, 305	eqtri 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))
307	306	reseq1i 5993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))
308		resundir 6012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)))
309	307, 308	eqtr2i 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({⟨(𝑀 + 1), (𝑀 + 1)⟩} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))
310		un0 4394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})
311	303, 309, 310	3eqtr3g 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))
312	251, 311	uneq12d 4169	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
313	215, 312	eqtrid 2789	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})))
314	313	fveq1d 6908	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
315	214, 314	sylan9eqr 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))
316	212, 315	oveq12d 7449	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))
317	316	mpteq2dva 5242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘𝑛) + (((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))))
318	317	uneq1d 4167	. . . . . . . . . . . 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 2783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘_f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {⟨(𝑀 + 1), 0⟩}))
320	319	uneq1d 4167	. . . . . . . . . 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 2780	. . . . . . . . 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 3903	. . . . . . . 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 2748	. . . . . . 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 3177	. . . . . 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 3178	. . . . 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 229	. . . 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 6849	. . . . . . . 8 ⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀))
328	11, 327	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 Fn (1...𝑀))
329	75, 75	fnsn 6624	. . . . . . . . 9 ⊢ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)}
330		fvun2 7001	. . . . . . . . 9 ⊢ ((𝑈 Fn (1...𝑀) ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
331	329, 330	mp3an2 1451	. . . . . . . 8 ⊢ ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)))
332	174, 331	mpanr2 704	. . . . . . 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 7201	. . . . . 6 ⊢ ({⟨(𝑀 + 1), (𝑀 + 1)⟩}‘(𝑀 + 1)) = (𝑀 + 1)
335	333, 334	eqtrdi 2793	. . . . 5 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1))
336	191, 335	jca 511	. . . 4 ⊢ (𝜑 → (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))
337	326, 336	jctird 526	. . 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	imbitrrdi 252	. 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 520	. . . . . 6 ⊢ (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {⟨(𝑀 + 1), 0⟩}:{(𝑀 + 1)}⟶{0}))
341	340, 92, 96	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}))
342	341, 114	mpbid 232	. . . 4 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
343		ovex 7464	. . . . 5 ⊢ (0..^𝐾) ∈ V
344		ovex 7464	. . . . 5 ⊢ (1...(𝑀 + 1)) ∈ V
345	343, 344	elmap 8911	. . . 4 ⊢ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑_m (1...(𝑀 + 1))) ↔ (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}):(1...(𝑀 + 1))⟶(0..^𝐾))
346	342, 345	sylibr 234	. . 3 ⊢ (𝜑 → (𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∈ ((0..^𝐾) ↑_m (1...(𝑀 + 1))))
347		ovex 7464	. . . . . . . 8 ⊢ (1...𝑀) ∈ V
348		f1oexrnex 7949	. . . . . . . 8 ⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V)
349	11, 347, 348	sylancl 586	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ V)
350		snex 5436	. . . . . . 7 ⊢ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V
351		unexg 7763	. . . . . . 7 ⊢ ((𝑈 ∈ V ∧ {⟨(𝑀 + 1), (𝑀 + 1)⟩} ∈ V) → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
352	349, 350, 351	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ V)
353		f1oeq1 6836	. . . . . . 7 ⊢ (𝑓 = (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))))
354	353	elabg 3676	. . . . . 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 6839	. . . . . 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 279	. . . 4 ⊢ (𝜑 → ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})))
359	126, 358	mpbird 257	. . 3 ⊢ (𝜑 → (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})
360	346, 359	opelxpd 5724	. 2 ⊢ (𝜑 → ⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑_m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}))
361	339, 360	jctild 525	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 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 {cab 2714 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ⦋csb 3899 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 {csn 4626 ⟨cop 4632 class class class wbr 5143 ↦ cmpt 5225 × cxp 5683 ^◡ccnv 5684 dom cdm 5685 ran crn 5686 ↾ cres 5687 “ cima 5688 Rel wrel 5690 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 ↑_m cmap 8866 0cc0 11155 1c1 11156 + caddc 11158 < clt 11295 ≤ cle 11296 − cmin 11492 ℕcn 12266 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 ...cfz 13547 ..^cfzo 13694

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-z 12614 df-uz 12879 df-fz 13548 df-fzo 13695

This theorem is referenced by: poimirlem4 37631

W3C validator