Metamath Proof Explorer

Theorem poimirlem3

Description: Lemma for poimir to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimirlem4.1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
poimirlem4.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
poimirlem4.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
poimirlem3.4 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑀 ) ⟶ ( 0 ..^ 𝐾 ) )
poimirlem3.5 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimirlem4.1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 poimirlem4.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 poimirlem4.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
5 poimirlem3.4 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑀 ) ⟶ ( 0 ..^ 𝐾 ) )
6 poimirlem3.5 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
7 5 ffnd ⊢ ( 𝜑 → 𝑇 Fn ( 1 ... 𝑀 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑇 Fn ( 1 ... 𝑀 ) )
9 1ex ⊢ 1 ∈ V
10 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) )
11 9 10 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) )
12 c0ex ⊢ 0 ∈ V
13 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
14 12 13 ax-mp ⊢ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) )
15 11 14 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
16 dff1o3 ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ↔ ( 𝑈 : ( 1 ... 𝑀 ) –onto→ ( 1 ... 𝑀 ) ∧ Fun ◡ 𝑈 ) )
17 16 simprbi ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → Fun ◡ 𝑈 )
18 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) )
19 6 17 18 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) )
20 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℕ0 )
21 20 nn0red ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ )
22 21 ltp1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 < ( 𝑗 + 1 ) )
23 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ∅ )
24 22 23 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ∅ )
25 24 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( 𝑈 “ ∅ ) )
26 ima0 ⊢ ( 𝑈 “ ∅ ) = ∅
27 25 26 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ∅ )
28 19 27 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ∅ )
29 fnun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) ∧ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) )
30 15 28 29 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) )
31 imaundi ⊢ ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
32 nn0p1nn ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
33 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
34 32 33 eleqtrdi ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
35 20 34 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
36 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑗 ) )
37 fzsplit2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 ... 𝑀 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
38 35 36 37 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 1 ... 𝑀 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
39 38 eqcomd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ( 1 ... 𝑀 ) )
40 39 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( 𝑈 “ ( 1 ... 𝑀 ) ) )
41 f1ofo ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → 𝑈 : ( 1 ... 𝑀 ) –onto→ ( 1 ... 𝑀 ) )
42 foima ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –onto→ ( 1 ... 𝑀 ) → ( 𝑈 “ ( 1 ... 𝑀 ) ) = ( 1 ... 𝑀 ) )
43 6 41 42 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑀 ) ) = ( 1 ... 𝑀 ) )
44 40 43 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( 1 ... 𝑀 ) )
45 31 44 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( 1 ... 𝑀 ) )
46 45 fneq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) ↔ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) Fn ( 1 ... 𝑀 ) ) )
47 30 46 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) Fn ( 1 ... 𝑀 ) )
48 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 1 ... 𝑀 ) ∈ V )
49 inidm ⊢ ( ( 1 ... 𝑀 ) ∩ ( 1 ... 𝑀 ) ) = ( 1 ... 𝑀 )
50 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
51 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) )
52 8 47 48 48 49 50 51 offval ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) )
53 nn0p1nn ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ )
54 3 53 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
55 54 nnzd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
56 uzid ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
57 peano2uz ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( ( 𝑀 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
58 55 56 57 3syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
59 3 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
60 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
61 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
62 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
63 eluz ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
64 62 63 sylan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
65 61 64 bitr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
66 59 60 65 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑁 ↔ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
67 4 66 mpbid ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
68 fzsplit2 ⊢ ( ( ( ( 𝑀 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ... 𝑁 ) = ( ( ( 𝑀 + 1 ) ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
69 58 67 68 syl2anc ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) = ( ( ( 𝑀 + 1 ) ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
70 fzsn ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( ( 𝑀 + 1 ) ... ( 𝑀 + 1 ) ) = { ( 𝑀 + 1 ) } )
71 55 70 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... ( 𝑀 + 1 ) ) = { ( 𝑀 + 1 ) } )
72 71 uneq1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) = ( { ( 𝑀 + 1 ) } ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
73 69 72 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) = ( { ( 𝑀 + 1 ) } ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
74 73 xpeq1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) ... 𝑁 ) × { 0 } ) = ( ( { ( 𝑀 + 1 ) } ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
75 xpundir ⊢ ( ( { ( 𝑀 + 1 ) } ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( { ( 𝑀 + 1 ) } × { 0 } ) ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) )
76 ovex ⊢ ( 𝑀 + 1 ) ∈ V
77 76 12 xpsn ⊢ ( { ( 𝑀 + 1 ) } × { 0 } ) = { ⟨ ( 𝑀 + 1 ) , 0 ⟩ }
78 77 uneq1i ⊢ ( ( { ( 𝑀 + 1 ) } × { 0 } ) ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) )
79 75 78 eqtri ⊢ ( ( { ( 𝑀 + 1 ) } ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) )
80 74 79 eqtrdi ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) ... 𝑁 ) × { 0 } ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑀 + 1 ) ... 𝑁 ) × { 0 } ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) )
82 52 81 uneq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) × { 0 } ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) ) )
83 unass ⊢ ( ( ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) )
84 82 83 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) × { 0 } ) ) = ( ( ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ∪ ( ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) × { 0 } ) ) )
85 3 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
86 85 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
87 54 nnred ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
88 85 87 ltnled ⊢ ( 𝜑 → ( 𝑀 < ( 𝑀 + 1 ) ↔ ¬ ( 𝑀 + 1 ) ≤ 𝑀 ) )
89 86 88 mpbid ⊢ ( 𝜑 → ¬ ( 𝑀 + 1 ) ≤ 𝑀 )
90 elfzle2 ⊢ ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑀 ) → ( 𝑀 + 1 ) ≤ 𝑀 )
91 89 90 nsyl ⊢ ( 𝜑 → ¬ ( 𝑀 + 1 ) ∈ ( 1 ... 𝑀 ) )
92 disjsn ⊢ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ↔ ¬ ( 𝑀 + 1 ) ∈ ( 1 ... 𝑀 ) )
93 91 92 sylibr ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ )
94 eqid ⊢ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } = { ⟨ ( 𝑀 + 1 ) , 0 ⟩ }
95 76 12 fsn ⊢ ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } : { ( 𝑀 + 1 ) } ⟶ { 0 } ↔ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } = { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } )
96 94 95 mpbir ⊢ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } : { ( 𝑀 + 1 ) } ⟶ { 0 }
97 fun ⊢ ( ( ( 𝑇 : ( 1 ... 𝑀 ) ⟶ ( 0 ..^ 𝐾 ) ∧ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } : { ( 𝑀 + 1 ) } ⟶ { 0 } ) ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ⟶ ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) )
98 96 97 mpanl2 ⊢ ( ( 𝑇 : ( 1 ... 𝑀 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ⟶ ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) )
99 5 93 98 syl2anc ⊢ ( 𝜑 → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ⟶ ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) )
100 1z ⊢ 1 ∈ ℤ
101 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
102 1m1e0 ⊢ ( 1 − 1 ) = 0
103 102 fveq2i ⊢ ( ℤ≥ ‘ ( 1 − 1 ) ) = ( ℤ≥ ‘ 0 )
104 101 103 eqtr4i ⊢ ℕ0 = ( ℤ≥ ‘ ( 1 − 1 ) )
105 3 104 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 1 − 1 ) ) )
106 fzsuc2 ⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ( ℤ≥ ‘ ( 1 − 1 ) ) ) → ( 1 ... ( 𝑀 + 1 ) ) = ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
107 100 105 106 sylancr ⊢ ( 𝜑 → ( 1 ... ( 𝑀 + 1 ) ) = ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
108 107 eqcomd ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) = ( 1 ... ( 𝑀 + 1 ) ) )
109 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝐾 ) ↔ 𝐾 ∈ ℕ )
110 2 109 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝐾 ) )
111 110 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 0 ..^ 𝐾 ) )
112 ssequn2 ⊢ ( { 0 } ⊆ ( 0 ..^ 𝐾 ) ↔ ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) = ( 0 ..^ 𝐾 ) )
113 111 112 sylib ⊢ ( 𝜑 → ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) = ( 0 ..^ 𝐾 ) )
114 108 113 feq23d ⊢ ( 𝜑 → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ⟶ ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) ↔ ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) ⟶ ( 0 ..^ 𝐾 ) ) )
115 99 114 mpbid ⊢ ( 𝜑 → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) ⟶ ( 0 ..^ 𝐾 ) )
116 115 ffnd ⊢ ( 𝜑 → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) Fn ( 1 ... ( 𝑀 + 1 ) ) )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) Fn ( 1 ... ( 𝑀 + 1 ) ) )
118 fnconstg ⊢ ( 1 ∈ V → ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) )
119 9 118 ax-mp ⊢ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) )
120 fnconstg ⊢ ( 0 ∈ V → ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) Fn ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
121 12 120 ax-mp ⊢ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) Fn ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) )
122 119 121 pm3.2i ⊢ ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∧ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) Fn ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
123 76 76 f1osn ⊢ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } : { ( 𝑀 + 1 ) } –1-1-onto→ { ( 𝑀 + 1 ) }
124 f1oun ⊢ ( ( ( 𝑈 : ( 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 ⊢ ( ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) ) → ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
126 6 93 93 125 syl12anc ⊢ ( 𝜑 → ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
127 dff1o3 ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ↔ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ∧ Fun ◡ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ) )
128 127 simprbi ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) → Fun ◡ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) )
129 imain ⊢ ( Fun ◡ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) = ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
130 126 128 129 3syl ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) = ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
131 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ∅ )
132 22 131 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ∅ )
133 132 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) = ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ∅ ) )
134 ima0 ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ∅ ) = ∅
135 133 134 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) = ∅ )
136 130 135 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) = ∅ )
137 fnun ⊢ ( ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) Fn ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
139 f1ofo ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) → ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
140 foima ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ) = ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
141 126 139 140 3syl ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ) = ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) )
142 107 imaeq2d ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... ( 𝑀 + 1 ) ) ) = ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ) )
143 141 142 107 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... ( 𝑀 + 1 ) ) ) = ( 1 ... ( 𝑀 + 1 ) ) )
144 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
145 36 144 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
146 fzsplit2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 ... ( 𝑀 + 1 ) ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
147 35 145 146 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 1 ... ( 𝑀 + 1 ) ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
148 147 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... ( 𝑀 + 1 ) ) ) = ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
149 143 148 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 1 ... ( 𝑀 + 1 ) ) = ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
150 imaundi ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) = ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
151 149 150 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 1 ... ( 𝑀 + 1 ) ) = ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
152 151 fneq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) Fn ( 1 ... ( 𝑀 + 1 ) ) )
154 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 1 ... ( 𝑀 + 1 ) ) ∈ V )
155 inidm ⊢ ( ( 1 ... ( 𝑀 + 1 ) ) ∩ ( 1 ... ( 𝑀 + 1 ) ) ) = ( 1 ... ( 𝑀 + 1 ) )
156 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... ( 𝑀 + 1 ) ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) )
157 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) “ dom ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) ) = ran ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } )
160 76 76 xpsn ⊢ ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) = { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ }
161 160 imaeq1i ⊢ ( ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) “ dom ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ dom ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) )
162 dmxpid ⊢ dom ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) = { ( 𝑀 + 1 ) }
163 162 imaeq2i ⊢ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ dom ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ { ( 𝑀 + 1 ) } )
164 161 163 eqtri ⊢ ( ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) “ dom ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ { ( 𝑀 + 1 ) } )
165 rnxpid ⊢ ran ( { ( 𝑀 + 1 ) } × { ( 𝑀 + 1 ) } ) = { ( 𝑀 + 1 ) }
166 159 164 165 3eqtr3ri ⊢ { ( 𝑀 + 1 ) } = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ { ( 𝑀 + 1 ) } )
167 eluzp1p1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
168 eluzfz2 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) → ( 𝑀 + 1 ) ∈ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) )
169 36 167 168 3syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) )
170 169 snssd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → { ( 𝑀 + 1 ) } ⊆ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) )
171 imass2 ⊢ ( { ( 𝑀 + 1 ) } ⊆ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) → ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ { ( 𝑀 + 1 ) } ) ⊆ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
172 170 171 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ { ( 𝑀 + 1 ) } ) ⊆ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
173 166 172 eqsstrid ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → { ( 𝑀 + 1 ) } ⊆ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
174 76 snid ⊢ ( 𝑀 + 1 ) ∈ { ( 𝑀 + 1 ) }
175 ssel ⊢ ( { ( 𝑀 + 1 ) } ⊆ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ∈ { ( 𝑀 + 1 ) } → ( 𝑀 + 1 ) ∈ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
176 173 174 175 mpisyl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑀 + 1 ) ∈ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
177 elun2 ⊢ ( ( 𝑀 + 1 ) ∈ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) → ( 𝑀 + 1 ) ∈ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
178 176 177 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) )
179 imaundir ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
180 178 179 eleqtrrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
181 180 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 + 1 ) ∈ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
182 12 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ∈ V )
183 108 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) = ( 1 ... ( 𝑀 + 1 ) ) )
184 fveq2 ⊢ ( 𝑛 = ( 𝑀 + 1 ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) )
185 76 12 fnsn ⊢ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } Fn { ( 𝑀 + 1 ) }
186 fvun2 ⊢ ( ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } Fn { ( 𝑀 + 1 ) } ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ ( 𝑀 + 1 ) ∈ { ( 𝑀 + 1 ) } ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ‘ ( 𝑀 + 1 ) ) )
187 185 186 mp3an2 ⊢ ( ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ ( 𝑀 + 1 ) ∈ { ( 𝑀 + 1 ) } ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ‘ ( 𝑀 + 1 ) ) )
188 174 187 mpanr2 ⊢ ( ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ‘ ( 𝑀 + 1 ) ) )
189 7 93 188 syl2anc ⊢ ( 𝜑 → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ‘ ( 𝑀 + 1 ) ) )
190 76 12 fvsn ⊢ ( { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ‘ ( 𝑀 + 1 ) ) = 0
191 189 190 eqtrdi ⊢ ( 𝜑 → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) = 0 )
192 184 191 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑛 = ( 𝑀 + 1 ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = 0 )
193 192 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 = ( 𝑀 + 1 ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = 0 )
194 fveq2 ⊢ ( 𝑛 = ( 𝑀 + 1 ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ ( 𝑀 + 1 ) ) )
195 fvun2 ⊢ ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 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 ⊢ ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ ( 𝑀 + 1 ) ) = ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ‘ ( 𝑀 + 1 ) ) )
198 12 fvconst2 ⊢ ( ( 𝑀 + 1 ) ∈ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ‘ ( 𝑀 + 1 ) ) = 0 )
199 180 198 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ‘ ( 𝑀 + 1 ) ) = 0 )
200 199 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ‘ ( 𝑀 + 1 ) ) = 0 )
201 197 200 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ ( 𝑀 + 1 ) ) = 0 )
202 194 201 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 = ( 𝑀 + 1 ) ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
203 193 202 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 = ( 𝑀 + 1 ) ) → ( ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) + ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) ) = ( 0 + 0 ) )
204 00id ⊢ ( 0 + 0 ) = 0
205 203 204 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 = ( 𝑀 + 1 ) ) → ( ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) + ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) ) = 0 )
206 181 182 183 205 fmptapd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 7 93 jca ⊢ ( 𝜑 → ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) )
208 fvun1 ⊢ ( ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } Fn { ( 𝑀 + 1 ) } ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
209 185 208 mp3an2 ⊢ ( ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
210 209 anassrs ⊢ ( ( ( 𝑇 Fn ( 1 ... 𝑀 ) ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
211 207 210 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
212 211 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
213 fvres ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → ( ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑛 ) = ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) )
214 213 eqcomd ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑛 ) )
215 resundir ⊢ ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) )
216 relxp ⊢ Rel ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } )
217 dmxpss ⊢ dom ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ⊆ ( 𝑈 “ ( 1 ... 𝑗 ) )
218 imassrn ⊢ ( 𝑈 “ ( 1 ... 𝑗 ) ) ⊆ ran 𝑈
219 217 218 sstri ⊢ dom ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ⊆ ran 𝑈
220 f1of ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → 𝑈 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
221 frn ⊢ ( 𝑈 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) → ran 𝑈 ⊆ ( 1 ... 𝑀 ) )
222 6 220 221 3syl ⊢ ( 𝜑 → ran 𝑈 ⊆ ( 1 ... 𝑀 ) )
223 219 222 sstrid ⊢ ( 𝜑 → dom ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ⊆ ( 1 ... 𝑀 ) )
224 relssres ⊢ ( ( Rel ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∧ dom ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ⊆ ( 1 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) )
225 216 223 224 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) )
226 225 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) )
227 imassrn ⊢ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ⊆ ran { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ }
228 76 rnsnop ⊢ ran { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } = { ( 𝑀 + 1 ) }
229 227 228 sseqtri ⊢ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ⊆ { ( 𝑀 + 1 ) }
230 ssrin ⊢ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ⊆ { ( 𝑀 + 1 ) } → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ( { ( 𝑀 + 1 ) } ∩ ( 1 ... 𝑀 ) ) )
231 229 230 ax-mp ⊢ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ( { ( 𝑀 + 1 ) } ∩ ( 1 ... 𝑀 ) )
232 incom ⊢ ( { ( 𝑀 + 1 ) } ∩ ( 1 ... 𝑀 ) ) = ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } )
233 232 93 syl5eq ⊢ ( 𝜑 → ( { ( 𝑀 + 1 ) } ∩ ( 1 ... 𝑀 ) ) = ∅ )
234 231 233 sseqtrid ⊢ ( 𝜑 → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ∅ )
235 ss0 ⊢ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ∅ → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
236 234 235 syl ⊢ ( 𝜑 → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
237 fnconstg ⊢ ( 1 ∈ V → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) )
238 fnresdisj ⊢ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) → ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ ↔ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ ) )
239 9 237 238 mp2b ⊢ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ ↔ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ )
240 236 239 sylib ⊢ ( 𝜑 → ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ )
241 240 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ )
242 226 241 uneq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ∅ ) )
243 imaundir ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) )
244 243 xpeq1i ⊢ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ) × { 1 } )
245 xpundir ⊢ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) ) × { 1 } ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) )
246 244 245 eqtri ⊢ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) )
247 246 reseq1i ⊢ ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ) ↾ ( 1 ... 𝑀 ) )
248 resundir ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) )
249 247 248 eqtr2i ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ) = ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) )
250 un0 ⊢ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ∅ ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } )
251 242 249 250 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) )
252 f1odm ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → dom 𝑈 = ( 1 ... 𝑀 ) )
253 6 252 syl ⊢ ( 𝜑 → dom 𝑈 = ( 1 ... 𝑀 ) )
254 253 ineq2d ⊢ ( 𝜑 → ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ dom 𝑈 ) = ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) )
255 254 reseq2d ⊢ ( 𝜑 → ( 𝑈 ↾ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ dom 𝑈 ) ) = ( 𝑈 ↾ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) ) )
256 f1orel ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → Rel 𝑈 )
257 resindm ⊢ ( Rel 𝑈 → ( 𝑈 ↾ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ dom 𝑈 ) ) = ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
258 6 256 257 3syl ⊢ ( 𝜑 → ( 𝑈 ↾ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ dom 𝑈 ) ) = ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
259 255 258 eqtr3d ⊢ ( 𝜑 → ( 𝑈 ↾ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) ) = ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
260 38 ineq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) = ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) )
261 fzssp1 ⊢ ( ( 𝑗 + 1 ) ... 𝑀 ) ⊆ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) )
262 sseqin2 ⊢ ( ( ( 𝑗 + 1 ) ... 𝑀 ) ⊆ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ↔ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ( ( 𝑗 + 1 ) ... 𝑀 ) )
263 261 262 mpbi ⊢ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ( ( 𝑗 + 1 ) ... 𝑀 )
264 263 a1i ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ( ( 𝑗 + 1 ) ... 𝑀 ) )
265 incom ⊢ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) = ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) )
266 265 132 syl5eq ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) = ∅ )
267 264 266 uneq12d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ∪ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) ) = ( ( ( 𝑗 + 1 ) ... 𝑀 ) ∪ ∅ ) )
268 uncom ⊢ ( ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ∪ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) ) = ( ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) ∪ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
269 indi ⊢ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) ∪ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
270 268 269 eqtr4i ⊢ ( ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ∪ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑗 ) ) ) = ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
271 un0 ⊢ ( ( ( 𝑗 + 1 ) ... 𝑀 ) ∪ ∅ ) = ( ( 𝑗 + 1 ) ... 𝑀 )
272 267 270 271 3eqtr3g ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ) = ( ( 𝑗 + 1 ) ... 𝑀 ) )
273 260 272 eqtrd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) = ( ( 𝑗 + 1 ) ... 𝑀 ) )
274 273 reseq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑈 ↾ ( ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) ) = ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
275 259 274 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
276 275 rneqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ran ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ran ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
277 df-ima ⊢ ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ran ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) )
278 df-ima ⊢ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) = ran ( 𝑈 ↾ ( ( 𝑗 + 1 ) ... 𝑀 ) )
279 276 277 278 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) = ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) )
280 279 xpeq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) )
281 280 reseq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) )
282 relxp ⊢ Rel ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } )
283 dmxpss ⊢ dom ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ⊆ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) )
284 imassrn ⊢ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) ⊆ ran 𝑈
285 283 284 sstri ⊢ dom ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ⊆ ran 𝑈
286 285 222 sstrid ⊢ ( 𝜑 → dom ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ⊆ ( 1 ... 𝑀 ) )
287 relssres ⊢ ( ( Rel ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ∧ dom ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ⊆ ( 1 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) )
288 282 286 287 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) )
289 288 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) )
290 281 289 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) )
291 imassrn ⊢ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ⊆ ran { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ }
292 291 228 sseqtri ⊢ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ⊆ { ( 𝑀 + 1 ) }
293 ssrin ⊢ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ⊆ { ( 𝑀 + 1 ) } → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ( { ( 𝑀 + 1 ) } ∩ ( 1 ... 𝑀 ) ) )
294 292 293 ax-mp ⊢ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ( { ( 𝑀 + 1 ) } ∩ ( 1 ... 𝑀 ) )
295 294 233 sseqtrid ⊢ ( 𝜑 → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ∅ )
296 ss0 ⊢ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) ⊆ ∅ → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
297 295 296 syl ⊢ ( 𝜑 → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
298 fnconstg ⊢ ( 0 ∈ V → ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) Fn ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) )
299 fnresdisj ⊢ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) Fn ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) → ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ ↔ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ ) )
300 12 298 299 mp2b ⊢ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ ↔ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ )
301 297 300 sylib ⊢ ( 𝜑 → ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ )
302 301 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ∅ )
303 290 302 uneq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ∪ ∅ ) )
304 179 xpeq1i ⊢ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) × { 0 } )
305 xpundir ⊢ ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ∪ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) ) × { 0 } ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) )
306 304 305 eqtri ⊢ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) )
307 306 reseq1i ⊢ ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) )
308 resundir ⊢ ( ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ∪ ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) )
309 307 308 eqtr2i ⊢ ( ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) ) = ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) )
310 un0 ⊢ ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ∪ ∅ ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } )
311 303 309 310 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) )
312 251 311 uneq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ↾ ( 1 ... 𝑀 ) ) ∪ ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ↾ ( 1 ... 𝑀 ) ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) )
313 215 312 syl5eq ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) )
314 313 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑛 ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) )
315 214 314 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) )
316 212 315 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) + ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) ) = ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) )
317 316 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ 𝑛 ) + ( ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) )
318 317 uneq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ∘f + ( ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) “ ( ( 𝑗 + 1 ) ... ( 𝑀 + 1 ) ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑇 ‘ 𝑛 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑀 ) ) × { 0 } ) ) ‘ 𝑛 ) ) ) ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) )
320 319 uneq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 84 320 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 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 ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 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 ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 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 ⊢ ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → 𝑈 Fn ( 1 ... 𝑀 ) )
328 6 327 syl ⊢ ( 𝜑 → 𝑈 Fn ( 1 ... 𝑀 ) )
329 76 76 fnsn ⊢ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } Fn { ( 𝑀 + 1 ) }
330 fvun2 ⊢ ( ( 𝑈 Fn ( 1 ... 𝑀 ) ∧ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } Fn { ( 𝑀 + 1 ) } ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ ( 𝑀 + 1 ) ∈ { ( 𝑀 + 1 ) } ) ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ‘ ( 𝑀 + 1 ) ) )
331 329 330 mp3an2 ⊢ ( ( 𝑈 Fn ( 1 ... 𝑀 ) ∧ ( ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ∧ ( 𝑀 + 1 ) ∈ { ( 𝑀 + 1 ) } ) ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ‘ ( 𝑀 + 1 ) ) )
332 174 331 mpanr2 ⊢ ( ( 𝑈 Fn ( 1 ... 𝑀 ) ∧ ( ( 1 ... 𝑀 ) ∩ { ( 𝑀 + 1 ) } ) = ∅ ) → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ‘ ( 𝑀 + 1 ) ) )
333 328 93 332 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ‘ ( 𝑀 + 1 ) ) )
334 76 76 fvsn ⊢ ( { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ‘ ( 𝑀 + 1 ) ) = ( 𝑀 + 1 )
335 333 334 eqtrdi ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( 𝑀 + 1 ) )
336 191 335 jca ⊢ ( 𝜑 → ( ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ‘ ( 𝑀 + 1 ) ) = 0 ∧ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ‘ ( 𝑀 + 1 ) ) = ( 𝑀 + 1 ) ) )
337 326 336 jctird ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 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 ⊢ ( ( ∀ 𝑖 ∈ ( 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 ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 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 5 96 jctir ⊢ ( 𝜑 → ( 𝑇 : ( 1 ... 𝑀 ) ⟶ ( 0 ..^ 𝐾 ) ∧ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } : { ( 𝑀 + 1 ) } ⟶ { 0 } ) )
341 340 93 97 syl2anc ⊢ ( 𝜑 → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ⟶ ( ( 0 ..^ 𝐾 ) ∪ { 0 } ) )
342 341 114 mpbid ⊢ ( 𝜑 → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) ⟶ ( 0 ..^ 𝐾 ) )
343 ovex ⊢ ( 0 ..^ 𝐾 ) ∈ V
344 ovex ⊢ ( 1 ... ( 𝑀 + 1 ) ) ∈ V
345 343 344 elmap ⊢ ( ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... ( 𝑀 + 1 ) ) ) ↔ ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) ⟶ ( 0 ..^ 𝐾 ) )
346 342 345 sylibr ⊢ ( 𝜑 → ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... ( 𝑀 + 1 ) ) ) )
347 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
348 f1oexrnex ⊢ ( ( 𝑈 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝑈 ∈ V )
349 6 347 348 sylancl ⊢ ( 𝜑 → 𝑈 ∈ V )
350 snex ⊢ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ∈ V
351 unexg ⊢ ( ( 𝑈 ∈ V ∧ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ∈ V ) → ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ∈ V )
352 349 350 351 sylancl ⊢ ( 𝜑 → ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ∈ V )
353 f1oeq1 ⊢ ( 𝑓 = ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) → ( 𝑓 : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) ↔ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) ) )
354 353 elabg ⊢ ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 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 ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) } ↔ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) ) )
356 f1oeq23 ⊢ ( ( ( 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 107 107 356 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) ↔ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ) )
358 355 357 bitrd ⊢ ( 𝜑 → ( ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) } ↔ ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) : ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑀 ) ∪ { ( 𝑀 + 1 ) } ) ) )
359 126 358 mpbird ⊢ ( 𝜑 → ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) } )
360 346 359 opelxpd ⊢ ( 𝜑 → ⟨ ( 𝑇 ∪ { ⟨ ( 𝑀 + 1 ) , 0 ⟩ } ) , ( 𝑈 ∪ { ⟨ ( 𝑀 + 1 ) , ( 𝑀 + 1 ) ⟩ } ) ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... ( 𝑀 + 1 ) ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... ( 𝑀 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 1 ) ) } ) )
361 339 360 jctild ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 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 ) ) ) ) )