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