This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdetunilem9

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a ⊢ A = N Mat R
mdetuni.b ⊢ B = Base A
mdetuni.k ⊢ K = Base R
mdetuni.0g ⊢ 0 ˙ = 0 R
mdetuni.1r ⊢ 1 ˙ = 1 R
mdetuni.pg ⊢ + ˙ = + R
mdetuni.tg ⊢ · ˙ = ⋅ R
mdetuni.n ⊢ φ → N ∈ Fin
mdetuni.r ⊢ φ → R ∈ Ring
mdetuni.ff ⊢ φ → D : B ⟶ K
mdetuni.al ⊢ φ → ∀ x ∈ B ∀ y ∈ N ∀ z ∈ N y ≠ z ∧ ∀ w ∈ N y x w = z x w → D ⁡ x = 0 ˙
mdetuni.li ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
mdetuni.sc ⊢ φ → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
mdetunilem9.id ⊢ φ → D ⁡ 1 A = 0 ˙
mdetunilem9.y ⊢ Y = x | ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
Assertion mdetunilem9 ⊢ φ → D = B × 0 ˙

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢ A = N Mat R
2 mdetuni.b ⊢ B = Base A
3 mdetuni.k ⊢ K = Base R
4 mdetuni.0g ⊢ 0 ˙ = 0 R
5 mdetuni.1r ⊢ 1 ˙ = 1 R
6 mdetuni.pg ⊢ + ˙ = + R
7 mdetuni.tg ⊢ · ˙ = ⋅ R
8 mdetuni.n ⊢ φ → N ∈ Fin
9 mdetuni.r ⊢ φ → R ∈ Ring
10 mdetuni.ff ⊢ φ → D : B ⟶ K
11 mdetuni.al ⊢ φ → ∀ x ∈ B ∀ y ∈ N ∀ z ∈ N y ≠ z ∧ ∀ w ∈ N y x w = z x w → D ⁡ x = 0 ˙
12 mdetuni.li ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
13 mdetuni.sc ⊢ φ → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
14 mdetunilem9.id ⊢ φ → D ⁡ 1 A = 0 ˙
15 mdetunilem9.y ⊢ Y = x | ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
16 ral0 ⊢ ∀ w ∈ ∅ a ⁡ w = if w ∈ I ↾ N 1 ˙ 0 ˙
17 simpr ⊢ φ ∧ a ∈ B → a ∈ B
18 f1oi ⊢ I ↾ N : N ⟶ 1-1 onto N
19 f1of ⊢ I ↾ N : N ⟶ 1-1 onto N → I ↾ N : N ⟶ N
20 18 19 mp1i ⊢ φ → I ↾ N : N ⟶ N
21 8 8 elmapd ⊢ φ → I ↾ N ∈ N N ↔ I ↾ N : N ⟶ N
22 20 21 mpbird ⊢ φ → I ↾ N ∈ N N
23 22 adantr ⊢ φ ∧ a ∈ B → I ↾ N ∈ N N
24 simplrl ⊢ φ ∧ y ∈ B ∧ z ∈ N N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → y ∈ B
25 1 3 2 matbas2i ⊢ y ∈ B → y ∈ K N × N
26 elmapi ⊢ y ∈ K N × N → y : N × N ⟶ K
27 25 26 syl ⊢ y ∈ B → y : N × N ⟶ K
28 27 feqmptd ⊢ y ∈ B → y = w ∈ N × N ⟼ y ⁡ w
29 28 fveq2d ⊢ y ∈ B → D ⁡ y = D ⁡ w ∈ N × N ⟼ y ⁡ w
30 24 29 syl ⊢ φ ∧ y ∈ B ∧ z ∈ N N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = D ⁡ w ∈ N × N ⟼ y ⁡ w
31 eqid ⊢ N × N = N × N
32 mpteq12 ⊢ N × N = N × N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → w ∈ N × N ⟼ y ⁡ w = w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙
33 32 fveq2d ⊢ N × N = N × N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ w ∈ N × N ⟼ y ⁡ w = D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙
34 31 33 mpan ⊢ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ w ∈ N × N ⟼ y ⁡ w = D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙
35 34 adantl ⊢ φ ∧ y ∈ B ∧ z ∈ N N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ w ∈ N × N ⟼ y ⁡ w = D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙
36 eleq1 ⊢ a = z → a ∈ N N ↔ z ∈ N N
37 36 anbi2d ⊢ a = z → φ ∧ a ∈ N N ↔ φ ∧ z ∈ N N
38 elequ2 ⊢ a = z → w ∈ a ↔ w ∈ z
39 38 ifbid ⊢ a = z → if w ∈ a 1 ˙ 0 ˙ = if w ∈ z 1 ˙ 0 ˙
40 39 mpteq2dv ⊢ a = z → w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙
41 40 fveq2d ⊢ a = z → D ⁡ w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙
42 41 eqeq1d ⊢ a = z → D ⁡ w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = 0 ˙ ↔ D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙ = 0 ˙
43 37 42 imbi12d ⊢ a = z → φ ∧ a ∈ N N → D ⁡ w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = 0 ˙ ↔ φ ∧ z ∈ N N → D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙ = 0 ˙
44 eleq1 ⊢ w = b c → w ∈ a ↔ b c ∈ a
45 44 ifbid ⊢ w = b c → if w ∈ a 1 ˙ 0 ˙ = if b c ∈ a 1 ˙ 0 ˙
46 45 mpompt ⊢ w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = b ∈ N , c ∈ N ⟼ if b c ∈ a 1 ˙ 0 ˙
47 elmapi ⊢ a ∈ N N → a : N ⟶ N
48 47 adantl ⊢ φ ∧ a ∈ N N → a : N ⟶ N
49 48 ffnd ⊢ φ ∧ a ∈ N N → a Fn N
50 49 3ad2ant1 ⊢ φ ∧ a ∈ N N ∧ b ∈ N ∧ c ∈ N → a Fn N
51 simp2 ⊢ φ ∧ a ∈ N N ∧ b ∈ N ∧ c ∈ N → b ∈ N
52 fnopfvb ⊢ a Fn N ∧ b ∈ N → a ⁡ b = c ↔ b c ∈ a
53 50 51 52 syl2anc ⊢ φ ∧ a ∈ N N ∧ b ∈ N ∧ c ∈ N → a ⁡ b = c ↔ b c ∈ a
54 53 bicomd ⊢ φ ∧ a ∈ N N ∧ b ∈ N ∧ c ∈ N → b c ∈ a ↔ a ⁡ b = c
55 54 ifbid ⊢ φ ∧ a ∈ N N ∧ b ∈ N ∧ c ∈ N → if b c ∈ a 1 ˙ 0 ˙ = if a ⁡ b = c 1 ˙ 0 ˙
56 55 mpoeq3dva ⊢ φ ∧ a ∈ N N → b ∈ N , c ∈ N ⟼ if b c ∈ a 1 ˙ 0 ˙ = b ∈ N , c ∈ N ⟼ if a ⁡ b = c 1 ˙ 0 ˙
57 46 56 eqtrid ⊢ φ ∧ a ∈ N N → w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = b ∈ N , c ∈ N ⟼ if a ⁡ b = c 1 ˙ 0 ˙
58 57 fveq2d ⊢ φ ∧ a ∈ N N → D ⁡ w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = D ⁡ b ∈ N , c ∈ N ⟼ if a ⁡ b = c 1 ˙ 0 ˙
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 mdetunilem8 ⊢ φ ∧ a : N ⟶ N → D ⁡ b ∈ N , c ∈ N ⟼ if a ⁡ b = c 1 ˙ 0 ˙ = 0 ˙
60 47 59 sylan2 ⊢ φ ∧ a ∈ N N → D ⁡ b ∈ N , c ∈ N ⟼ if a ⁡ b = c 1 ˙ 0 ˙ = 0 ˙
61 58 60 eqtrd ⊢ φ ∧ a ∈ N N → D ⁡ w ∈ N × N ⟼ if w ∈ a 1 ˙ 0 ˙ = 0 ˙
62 43 61 chvarvv ⊢ φ ∧ z ∈ N N → D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙ = 0 ˙
63 62 adantrl ⊢ φ ∧ y ∈ B ∧ z ∈ N N → D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙ = 0 ˙
64 63 adantr ⊢ φ ∧ y ∈ B ∧ z ∈ N N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ w ∈ N × N ⟼ if w ∈ z 1 ˙ 0 ˙ = 0 ˙
65 30 35 64 3eqtrd ⊢ φ ∧ y ∈ B ∧ z ∈ N N ∧ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
66 65 ex ⊢ φ ∧ y ∈ B ∧ z ∈ N N → ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
67 66 ralrimivva ⊢ φ → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
68 xpfi ⊢ N ∈ Fin ∧ N ∈ Fin → N × N ∈ Fin
69 8 8 68 syl2anc ⊢ φ → N × N ∈ Fin
70 raleq ⊢ x = N × N → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙
71 70 imbi1d ⊢ x = N × N → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
72 71 2ralbidv ⊢ x = N × N → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
73 72 15 elab2g ⊢ N × N ∈ Fin → N × N ∈ Y ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
74 69 73 syl ⊢ φ → N × N ∈ Y ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ N × N y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
75 67 74 mpbird ⊢ φ → N × N ∈ Y
76 ssid ⊢ N × N ⊆ N × N
77 69 3ad2ant1 ⊢ φ ∧ N × N ⊆ N × N ∧ ¬ ∅ ∈ Y → N × N ∈ Fin
78 sseq1 ⊢ a = ∅ → a ⊆ N × N ↔ ∅ ⊆ N × N
79 78 3anbi2d ⊢ a = ∅ → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y ↔ φ ∧ ∅ ⊆ N × N ∧ ¬ ∅ ∈ Y
80 eleq1 ⊢ a = ∅ → a ∈ Y ↔ ∅ ∈ Y
81 80 notbid ⊢ a = ∅ → ¬ a ∈ Y ↔ ¬ ∅ ∈ Y
82 79 81 imbi12d ⊢ a = ∅ → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ a ∈ Y ↔ φ ∧ ∅ ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ ∅ ∈ Y
83 sseq1 ⊢ a = b → a ⊆ N × N ↔ b ⊆ N × N
84 83 3anbi2d ⊢ a = b → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y ↔ φ ∧ b ⊆ N × N ∧ ¬ ∅ ∈ Y
85 eleq1 ⊢ a = b → a ∈ Y ↔ b ∈ Y
86 85 notbid ⊢ a = b → ¬ a ∈ Y ↔ ¬ b ∈ Y
87 84 86 imbi12d ⊢ a = b → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ a ∈ Y ↔ φ ∧ b ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y
88 sseq1 ⊢ a = b ∪ c → a ⊆ N × N ↔ b ∪ c ⊆ N × N
89 88 3anbi2d ⊢ a = b ∪ c → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y ↔ φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y
90 eleq1 ⊢ a = b ∪ c → a ∈ Y ↔ b ∪ c ∈ Y
91 90 notbid ⊢ a = b ∪ c → ¬ a ∈ Y ↔ ¬ b ∪ c ∈ Y
92 89 91 imbi12d ⊢ a = b ∪ c → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ a ∈ Y ↔ φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∪ c ∈ Y
93 sseq1 ⊢ a = N × N → a ⊆ N × N ↔ N × N ⊆ N × N
94 93 3anbi2d ⊢ a = N × N → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y ↔ φ ∧ N × N ⊆ N × N ∧ ¬ ∅ ∈ Y
95 eleq1 ⊢ a = N × N → a ∈ Y ↔ N × N ∈ Y
96 95 notbid ⊢ a = N × N → ¬ a ∈ Y ↔ ¬ N × N ∈ Y
97 94 96 imbi12d ⊢ a = N × N → φ ∧ a ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ a ∈ Y ↔ φ ∧ N × N ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ N × N ∈ Y
98 simp3 ⊢ φ ∧ ∅ ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ ∅ ∈ Y
99 ssun1 ⊢ b ⊆ b ∪ c
100 sstr2 ⊢ b ⊆ b ∪ c → b ∪ c ⊆ N × N → b ⊆ N × N
101 99 100 ax-mp ⊢ b ∪ c ⊆ N × N → b ⊆ N × N
102 101 3anim2i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → φ ∧ b ⊆ N × N ∧ ¬ ∅ ∈ Y
103 102 imim1i ⊢ φ ∧ b ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y → φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y
104 simpl1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → φ
105 simpl2 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → b ∪ c ⊆ N × N
106 simprll ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → a ∈ B
107 1 3 2 matbas2i ⊢ a ∈ B → a ∈ K N × N
108 elmapi ⊢ a ∈ K N × N → a : N × N ⟶ K
109 107 108 syl ⊢ a ∈ B → a : N × N ⟶ K
110 109 3ad2ant3 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a : N × N ⟶ K
111 110 feqmptd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a = e ∈ N × N ⟼ a ⁡ e
112 111 reseq1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ a ⁡ e ↾ 1 st ⁡ c × N
113 9 3ad2ant1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → R ∈ Ring
114 ringgrp ⊢ R ∈ Ring → R ∈ Grp
115 113 114 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → R ∈ Grp
116 115 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → R ∈ Grp
117 110 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a : N × N ⟶ K
118 simp2 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → b ∪ c ⊆ N × N
119 118 unssbd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → c ⊆ N × N
120 vex ⊢ c ∈ V
121 120 snss ⊢ c ∈ N × N ↔ c ⊆ N × N
122 119 121 sylibr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → c ∈ N × N
123 xp1st ⊢ c ∈ N × N → 1 st ⁡ c ∈ N
124 122 123 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 st ⁡ c ∈ N
125 124 snssd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 st ⁡ c ⊆ N
126 xpss1 ⊢ 1 st ⁡ c ⊆ N → 1 st ⁡ c × N ⊆ N × N
127 125 126 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 st ⁡ c × N ⊆ N × N
128 127 sselda ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → e ∈ N × N
129 117 128 ffvelcdmd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ e ∈ K
130 3 5 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ K
131 113 130 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 ˙ ∈ K
132 3 4 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ K
133 113 132 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 0 ˙ ∈ K
134 131 133 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → if e ∈ d 1 ˙ 0 ˙ ∈ K
135 134 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if e ∈ d 1 ˙ 0 ˙ ∈ K
136 eqid ⊢ - R = - R
137 3 6 136 grpnpcan ⊢ R ∈ Grp ∧ a ⁡ e ∈ K ∧ if e ∈ d 1 ˙ 0 ˙ ∈ K → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ + ˙ if e ∈ d 1 ˙ 0 ˙ = a ⁡ e
138 116 129 135 137 syl3anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ + ˙ if e ∈ d 1 ˙ 0 ˙ = a ⁡ e
139 138 eqcomd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ e = a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ + ˙ if e ∈ d 1 ˙ 0 ˙
140 139 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → a ⁡ e = a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ + ˙ if e ∈ d 1 ˙ 0 ˙
141 iftrue ⊢ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = a ⁡ e - R if e ∈ d 1 ˙ 0 ˙
142 iftrue ⊢ e = c → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = if e ∈ d 1 ˙ 0 ˙
143 141 142 oveq12d ⊢ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ + ˙ if e ∈ d 1 ˙ 0 ˙
144 143 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ + ˙ if e ∈ d 1 ˙ 0 ˙
145 140 144 eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → a ⁡ e = if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
146 3 6 4 grplid ⊢ R ∈ Grp ∧ a ⁡ e ∈ K → 0 ˙ + ˙ a ⁡ e = a ⁡ e
147 116 129 146 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → 0 ˙ + ˙ a ⁡ e = a ⁡ e
148 147 eqcomd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ e = 0 ˙ + ˙ a ⁡ e
149 148 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → a ⁡ e = 0 ˙ + ˙ a ⁡ e
150 iffalse ⊢ ¬ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = 0 ˙
151 iffalse ⊢ ¬ e = c → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ e
152 150 151 oveq12d ⊢ ¬ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙ + ˙ a ⁡ e
153 152 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙ + ˙ a ⁡ e
154 149 153 eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → a ⁡ e = if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
155 145 154 pm2.61dan ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ e = if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
156 155 mpteq2dva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ 1 st ⁡ c × N ⟼ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
157 snfi ⊢ 1 st ⁡ c ∈ Fin
158 8 3ad2ant1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → N ∈ Fin
159 xpfi ⊢ 1 st ⁡ c ∈ Fin ∧ N ∈ Fin → 1 st ⁡ c × N ∈ Fin
160 157 158 159 sylancr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 st ⁡ c × N ∈ Fin
161 ovex ⊢ a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ ∈ V
162 4 fvexi ⊢ 0 ˙ ∈ V
163 161 162 ifex ⊢ if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ ∈ V
164 163 a1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ ∈ V
165 5 fvexi ⊢ 1 ˙ ∈ V
166 165 162 ifex ⊢ if e ∈ d 1 ˙ 0 ˙ ∈ V
167 fvex ⊢ a ⁡ e ∈ V
168 166 167 ifex ⊢ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ V
169 168 a1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ V
170 xp1st ⊢ e ∈ 1 st ⁡ c × N → 1 st ⁡ e ∈ 1 st ⁡ c
171 elsni ⊢ 1 st ⁡ e ∈ 1 st ⁡ c → 1 st ⁡ e = 1 st ⁡ c
172 iftrue ⊢ 1 st ⁡ e = 1 st ⁡ c → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙
173 170 171 172 3syl ⊢ e ∈ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙
174 173 mpteq2ia ⊢ e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙
175 174 a1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙
176 eqidd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
177 160 164 169 175 176 offval2 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ f e ∈ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ + ˙ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
178 156 177 eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ 1 st ⁡ c × N ⟼ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ f e ∈ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
179 127 resmptd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ 1 st ⁡ c × N ⟼ a ⁡ e
180 127 resmptd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e
181 127 resmptd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
182 180 181 oveq12d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ f e ∈ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
183 178 179 182 3eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
184 112 183 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
185 111 reseq1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
186 xp1st ⊢ e ∈ N ∖ 1 st ⁡ c × N → 1 st ⁡ e ∈ N ∖ 1 st ⁡ c
187 eldifsni ⊢ 1 st ⁡ e ∈ N ∖ 1 st ⁡ c → 1 st ⁡ e ≠ 1 st ⁡ c
188 186 187 syl ⊢ e ∈ N ∖ 1 st ⁡ c × N → 1 st ⁡ e ≠ 1 st ⁡ c
189 188 neneqd ⊢ e ∈ N ∖ 1 st ⁡ c × N → ¬ 1 st ⁡ e = 1 st ⁡ c
190 189 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N ∖ 1 st ⁡ c × N → ¬ 1 st ⁡ e = 1 st ⁡ c
191 190 iffalsed ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N ∖ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ e
192 191 mpteq2dva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = e ∈ N ∖ 1 st ⁡ c × N ⟼ a ⁡ e
193 difss ⊢ N ∖ 1 st ⁡ c ⊆ N
194 xpss1 ⊢ N ∖ 1 st ⁡ c ⊆ N → N ∖ 1 st ⁡ c × N ⊆ N × N
195 193 194 ax-mp ⊢ N ∖ 1 st ⁡ c × N ⊆ N × N
196 resmpt ⊢ N ∖ 1 st ⁡ c × N ⊆ N × N → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e
197 195 196 mp1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e
198 resmpt ⊢ N ∖ 1 st ⁡ c × N ⊆ N × N → e ∈ N × N ⟼ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ a ⁡ e
199 195 198 mp1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ a ⁡ e
200 192 197 199 3eqtr4rd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
201 185 200 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
202 fveq2 ⊢ e = c → 1 st ⁡ e = 1 st ⁡ c
203 190 202 nsyl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N ∖ 1 st ⁡ c × N → ¬ e = c
204 203 iffalsed ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N ∖ 1 st ⁡ c × N → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ e
205 204 mpteq2dva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N ∖ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = e ∈ N ∖ 1 st ⁡ c × N ⟼ a ⁡ e
206 resmpt ⊢ N ∖ 1 st ⁡ c × N ⊆ N × N → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
207 195 206 mp1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
208 205 207 199 3eqtr4rd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
209 185 208 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
210 134 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → if e ∈ d 1 ˙ 0 ˙ ∈ K
211 110 ffvelcdmda ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → a ⁡ e ∈ K
212 210 211 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ K
213 212 fmpttd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
214 3 fvexi ⊢ K ∈ V
215 68 anidms ⊢ N ∈ Fin → N × N ∈ Fin
216 158 215 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → N × N ∈ Fin
217 elmapg ⊢ K ∈ V ∧ N × N ∈ Fin → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ K N × N ↔ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
218 214 216 217 sylancr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ K N × N ↔ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
219 213 218 mpbird ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ K N × N
220 1 3 matbas2 ⊢ N ∈ Fin ∧ R ∈ Ring → K N × N = Base A
221 158 113 220 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → K N × N = Base A
222 221 2 eqtr4di ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → K N × N = B
223 219 222 eleqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ B
224 simp3 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ∈ B
225 115 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → R ∈ Grp
226 3 136 grpsubcl ⊢ R ∈ Grp ∧ a ⁡ e ∈ K ∧ if e ∈ d 1 ˙ 0 ˙ ∈ K → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ ∈ K
227 225 211 210 226 syl3anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ ∈ K
228 133 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → 0 ˙ ∈ K
229 227 228 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ ∈ K
230 229 211 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ K
231 230 fmpttd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
232 elmapg ⊢ K ∈ V ∧ N × N ∈ Fin → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ K N × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
233 214 216 232 sylancr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ K N × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
234 231 233 mpbird ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ K N × N
235 234 222 eleqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ B
236 12 3ad2ant1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
237 reseq1 ⊢ x = a → x ↾ w × N = a ↾ w × N
238 237 eqeq1d ⊢ x = a → x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ↔ a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N
239 reseq1 ⊢ x = a → x ↾ N ∖ w × N = a ↾ N ∖ w × N
240 239 eqeq1d ⊢ x = a → x ↾ N ∖ w × N = y ↾ N ∖ w × N ↔ a ↾ N ∖ w × N = y ↾ N ∖ w × N
241 239 eqeq1d ⊢ x = a → x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ a ↾ N ∖ w × N = z ↾ N ∖ w × N
242 238 240 241 3anbi123d ⊢ x = a → x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N
243 fveqeq2 ⊢ x = a → D ⁡ x = D ⁡ y + ˙ D ⁡ z ↔ D ⁡ a = D ⁡ y + ˙ D ⁡ z
244 242 243 imbi12d ⊢ x = a → x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z ↔ a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ y + ˙ D ⁡ z
245 244 2ralbidv ⊢ x = a → ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ y + ˙ D ⁡ z
246 reseq1 ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → y ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N
247 246 oveq1d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → y ↾ w × N + ˙ f z ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N
248 247 eqeq2d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ↔ a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N
249 reseq1 ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → y ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
250 249 eqeq2d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → a ↾ N ∖ w × N = y ↾ N ∖ w × N ↔ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
251 248 250 3anbi12d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N
252 fveq2 ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → D ⁡ y = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e
253 252 oveq1d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → D ⁡ y + ˙ D ⁡ z = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z
254 253 eqeq2d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → D ⁡ a = D ⁡ y + ˙ D ⁡ z ↔ D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z
255 251 254 imbi12d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ y + ˙ D ⁡ z ↔ a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z
256 255 2ralbidv ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → ∀ z ∈ B ∀ w ∈ N a ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ y + ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z
257 245 256 rspc2va ⊢ a ∈ B ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ B ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z → ∀ z ∈ B ∀ w ∈ N a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z
258 224 235 236 257 syl21anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → ∀ z ∈ B ∀ w ∈ N a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z
259 reseq1 ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → z ↾ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N
260 259 oveq2d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N
261 260 eqeq2d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ↔ a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N
262 reseq1 ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → z ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
263 262 eqeq2d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → a ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ a ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
264 261 263 3anbi13d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
265 fveq2 ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → D ⁡ z = D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
266 265 oveq2d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
267 266 eqeq2d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z ↔ D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
268 264 267 imbi12d ⊢ z = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z ↔ a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
269 sneq ⊢ w = 1 st ⁡ c → w = 1 st ⁡ c
270 269 xpeq1d ⊢ w = 1 st ⁡ c → w × N = 1 st ⁡ c × N
271 270 reseq2d ⊢ w = 1 st ⁡ c → a ↾ w × N = a ↾ 1 st ⁡ c × N
272 270 reseq2d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
273 270 reseq2d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
274 272 273 oveq12d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
275 271 274 eqeq12d ⊢ w = 1 st ⁡ c → a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N ↔ a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
276 269 difeq2d ⊢ w = 1 st ⁡ c → N ∖ w = N ∖ 1 st ⁡ c
277 276 xpeq1d ⊢ w = 1 st ⁡ c → N ∖ w × N = N ∖ 1 st ⁡ c × N
278 277 reseq2d ⊢ w = 1 st ⁡ c → a ↾ N ∖ w × N = a ↾ N ∖ 1 st ⁡ c × N
279 277 reseq2d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
280 278 279 eqeq12d ⊢ w = 1 st ⁡ c → a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ↔ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
281 277 reseq2d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
282 278 281 eqeq12d ⊢ w = 1 st ⁡ c → a ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ↔ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
283 275 280 282 3anbi123d ⊢ w = 1 st ⁡ c → a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ↔ a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
284 283 imbi1d ⊢ w = 1 st ⁡ c → a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↔ a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
285 268 284 rspc2va ⊢ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ B ∧ 1 st ⁡ c ∈ N ∧ ∀ z ∈ B ∀ w ∈ N a ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N + ˙ f z ↾ w × N ∧ a ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ∧ a ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ z → a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
286 223 124 258 285 syl21anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ↾ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N + ˙ f e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N ∧ a ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
287 184 201 209 286 mp3and ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
288 104 105 106 287 syl3anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ a = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
289 fveq2 ⊢ e = c → a ⁡ e = a ⁡ c
290 elequ1 ⊢ e = c → e ∈ d ↔ c ∈ d
291 290 ifbid ⊢ e = c → if e ∈ d 1 ˙ 0 ˙ = if c ∈ d 1 ˙ 0 ˙
292 289 291 oveq12d ⊢ e = c → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
293 292 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
294 110 122 ffvelcdmd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ⁡ c ∈ K
295 131 133 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → if c ∈ d 1 ˙ 0 ˙ ∈ K
296 3 136 grpsubcl ⊢ R ∈ Grp ∧ a ⁡ c ∈ K ∧ if c ∈ d 1 ˙ 0 ˙ ∈ K → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ ∈ K
297 115 294 295 296 syl3anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ ∈ K
298 3 7 5 ringridm ⊢ R ∈ Ring ∧ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ ∈ K → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 1 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
299 113 297 298 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 1 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
300 299 ad2antrr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 1 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
301 293 300 eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 1 ˙
302 141 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = a ⁡ e - R if e ∈ d 1 ˙ 0 ˙
303 iftrue ⊢ e = c → if e = c 1 ˙ 0 ˙ = 1 ˙
304 303 oveq2d ⊢ e = c → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 1 ˙
305 304 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 1 ˙
306 301 302 305 3eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙
307 3 7 4 ringrz ⊢ R ∈ Ring ∧ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ ∈ K → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙ = 0 ˙
308 113 297 307 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙ = 0 ˙
309 308 eqcomd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙
310 309 ad2antrr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙
311 150 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = 0 ˙
312 iffalse ⊢ ¬ e = c → if e = c 1 ˙ 0 ˙ = 0 ˙
313 312 oveq2d ⊢ ¬ e = c → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙
314 313 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙
315 310 311 314 3eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N ∧ ¬ e = c → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙
316 306 315 pm2.61dan ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙
317 170 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → 1 st ⁡ e ∈ 1 st ⁡ c
318 317 171 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → 1 st ⁡ e = 1 st ⁡ c
319 318 iftrued ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙
320 318 iftrued ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = if e = c 1 ˙ 0 ˙
321 320 oveq2d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if e = c 1 ˙ 0 ˙
322 316 319 321 3eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
323 322 mpteq2dva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = e ∈ 1 st ⁡ c × N ⟼ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
324 ovexd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ ∈ V
325 165 162 ifex ⊢ if e = c 1 ˙ 0 ˙ ∈ V
326 325 167 ifex ⊢ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ V
327 326 a1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ V
328 fconstmpt ⊢ 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ = e ∈ 1 st ⁡ c × N ⟼ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
329 328 a1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ = e ∈ 1 st ⁡ c × N ⟼ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
330 127 resmptd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
331 160 324 327 329 330 offval2 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = e ∈ 1 st ⁡ c × N ⟼ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
332 323 180 331 3eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
333 iffalse ⊢ ¬ 1 st ⁡ e = 1 st ⁡ c → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ e
334 iffalse ⊢ ¬ 1 st ⁡ e = 1 st ⁡ c → if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = a ⁡ e
335 333 334 eqtr4d ⊢ ¬ 1 st ⁡ e = 1 st ⁡ c → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
336 190 335 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N ∖ 1 st ⁡ c × N → if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
337 336 mpteq2dva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
338 resmpt ⊢ N ∖ 1 st ⁡ c × N ⊆ N × N → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
339 195 338 mp1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N ∖ 1 st ⁡ c × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
340 337 197 339 3eqtr4d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
341 131 133 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → if e = c 1 ˙ 0 ˙ ∈ K
342 341 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → if e = c 1 ˙ 0 ˙ ∈ K
343 342 211 ifcld ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ e ∈ N × N → if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ K
344 343 fmpttd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
345 elmapg ⊢ K ∈ V ∧ N × N ∈ Fin → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ K N × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
346 214 216 345 sylancr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ K N × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e : N × N ⟶ K
347 344 346 mpbird ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ K N × N
348 347 222 eleqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ B
349 13 3ad2ant1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
350 reseq1 ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → x ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N
351 350 eqeq1d ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → x ↾ w × N = w × N × y · ˙ f z ↾ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N
352 reseq1 ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → x ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
353 352 eqeq1d ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N
354 351 353 anbi12d ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N
355 fveqeq2 ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → D ⁡ x = y · ˙ D ⁡ z ↔ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = y · ˙ D ⁡ z
356 354 355 imbi12d ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = y · ˙ D ⁡ z
357 356 2ralbidv ⊢ x = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e → ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = y · ˙ D ⁡ z
358 sneq ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
359 358 xpeq2d ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → w × N × y = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
360 359 oveq1d ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → w × N × y · ˙ f z ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N
361 360 eqeq2d ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N
362 361 anbi1d ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N
363 oveq1 ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → y · ˙ D ⁡ z = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z
364 363 eqeq2d ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = y · ˙ D ⁡ z ↔ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z
365 362 364 imbi12d ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = y · ˙ D ⁡ z ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z
366 365 2ralbidv ⊢ y = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ → ∀ z ∈ B ∀ w ∈ N e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = y · ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z
367 357 366 rspc2va ⊢ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ∈ B ∧ a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ ∈ K ∧ ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z → ∀ z ∈ B ∀ w ∈ N e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z
368 235 297 349 367 syl21anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → ∀ z ∈ B ∀ w ∈ N e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z
369 reseq1 ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → z ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N
370 369 oveq2d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N
371 370 eqeq2d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N
372 reseq1 ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → z ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
373 372 eqeq2d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
374 371 373 anbi12d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N
375 fveq2 ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → D ⁡ z = D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
376 375 oveq2d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
377 376 eqeq2d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z ↔ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
378 374 377 imbi12d ⊢ z = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
379 270 xpeq1d ⊢ w = 1 st ⁡ c → w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙
380 270 reseq2d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
381 379 380 oveq12d ⊢ w = 1 st ⁡ c → w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
382 272 381 eqeq12d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N
383 277 reseq2d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
384 279 383 eqeq12d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
385 382 384 anbi12d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N
386 385 imbi1d ⊢ w = 1 st ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
387 378 386 rspc2va ⊢ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ B ∧ 1 st ⁡ c ∈ N ∧ ∀ z ∈ B ∀ w ∈ N e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ w × N = w × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f z ↾ w × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ z → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
388 348 124 368 387 syl21anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N = 1 st ⁡ c × N × a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ f e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ 1 st ⁡ c × N ∧ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ↾ N ∖ 1 st ⁡ c × N → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
389 332 340 388 mp2and ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
390 389 oveq1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
391 104 105 106 390 syl3anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c a ⁡ e - R if e ∈ d 1 ˙ 0 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
392 simpl3 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → b ∪ c ∈ Y
393 simprlr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → d ∈ N N
394 simprr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙
395 ralss ⊢ b ⊆ b ∪ c → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙
396 99 395 ax-mp ⊢ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙
397 iftrue ⊢ 1 st ⁡ w = 1 st ⁡ c → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w = c 1 ˙ 0 ˙
398 397 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w = c 1 ˙ 0 ˙
399 ibar ⊢ 1 st ⁡ w = 1 st ⁡ c → 2 nd ⁡ w = 2 nd ⁡ c ↔ 1 st ⁡ w = 1 st ⁡ c ∧ 2 nd ⁡ w = 2 nd ⁡ c
400 399 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → 2 nd ⁡ w = 2 nd ⁡ c ↔ 1 st ⁡ w = 1 st ⁡ c ∧ 2 nd ⁡ w = 2 nd ⁡ c
401 relxp ⊢ Rel ⁡ N × N
402 simpl2 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → b ∪ c ⊆ N × N
403 402 sselda ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c → w ∈ N × N
404 403 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → w ∈ N × N
405 1st2nd ⊢ Rel ⁡ N × N ∧ w ∈ N × N → w = 1 st ⁡ w 2 nd ⁡ w
406 401 404 405 sylancr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → w = 1 st ⁡ w 2 nd ⁡ w
407 406 eleq1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
408 simpr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → d ∈ N N
409 elmapi ⊢ d ∈ N N → d : N ⟶ N
410 409 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → d : N ⟶ N
411 124 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → 1 st ⁡ c ∈ N
412 xp2nd ⊢ c ∈ N × N → 2 nd ⁡ c ∈ N
413 122 412 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 2 nd ⁡ c ∈ N
414 413 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → 2 nd ⁡ c ∈ N
415 fsets ⊢ d ∈ N N ∧ d : N ⟶ N ∧ 1 st ⁡ c ∈ N ∧ 2 nd ⁡ c ∈ N → d sSet 1 st ⁡ c 2 nd ⁡ c : N ⟶ N
416 408 410 411 414 415 syl211anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → d sSet 1 st ⁡ c 2 nd ⁡ c : N ⟶ N
417 416 ffnd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → d sSet 1 st ⁡ c 2 nd ⁡ c Fn N
418 417 ad2antrr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c Fn N
419 xp1st ⊢ w ∈ N × N → 1 st ⁡ w ∈ N
420 403 419 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c → 1 st ⁡ w ∈ N
421 420 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w ∈ N
422 fnopfvb ⊢ d sSet 1 st ⁡ c 2 nd ⁡ c Fn N ∧ 1 st ⁡ w ∈ N → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = 2 nd ⁡ w ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
423 418 421 422 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = 2 nd ⁡ w ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
424 fveq2 ⊢ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ c
425 424 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ c
426 vex ⊢ d ∈ V
427 fvex ⊢ 1 st ⁡ c ∈ V
428 fvex ⊢ 2 nd ⁡ c ∈ V
429 fvsetsid ⊢ d ∈ V ∧ 1 st ⁡ c ∈ V ∧ 2 nd ⁡ c ∈ V → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ c = 2 nd ⁡ c
430 426 427 428 429 mp3an ⊢ d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ c = 2 nd ⁡ c
431 425 430 eqtrdi ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = 2 nd ⁡ c
432 431 eqeq1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = 2 nd ⁡ w ↔ 2 nd ⁡ c = 2 nd ⁡ w
433 eqcom ⊢ 2 nd ⁡ c = 2 nd ⁡ w ↔ 2 nd ⁡ w = 2 nd ⁡ c
434 432 433 bitrdi ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → d sSet 1 st ⁡ c 2 nd ⁡ c ⁡ 1 st ⁡ w = 2 nd ⁡ w ↔ 2 nd ⁡ w = 2 nd ⁡ c
435 407 423 434 3bitr2rd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → 2 nd ⁡ w = 2 nd ⁡ c ↔ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
436 122 ad3antrrr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → c ∈ N × N
437 xpopth ⊢ w ∈ N × N ∧ c ∈ N × N → 1 st ⁡ w = 1 st ⁡ c ∧ 2 nd ⁡ w = 2 nd ⁡ c ↔ w = c
438 404 436 437 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w = 1 st ⁡ c ∧ 2 nd ⁡ w = 2 nd ⁡ c ↔ w = c
439 400 435 438 3bitr3rd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → w = c ↔ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
440 439 ifbid ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → if w = c 1 ˙ 0 ˙ = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
441 398 440 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
442 441 a1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ 1 st ⁡ w = 1 st ⁡ c → w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
443 elsni ⊢ w ∈ c → w = c
444 443 fveq2d ⊢ w ∈ c → 1 st ⁡ w = 1 st ⁡ c
445 444 con3i ⊢ ¬ 1 st ⁡ w = 1 st ⁡ c → ¬ w ∈ c
446 445 adantl ⊢ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → ¬ w ∈ c
447 elun ⊢ w ∈ b ∪ c ↔ w ∈ b ∨ w ∈ c
448 447 birani ⊢ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → w ∈ b ∨ w ∈ c
449 orel2 ⊢ ¬ w ∈ c → w ∈ b ∨ w ∈ c → w ∈ b
450 446 448 449 sylc ⊢ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → w ∈ b
451 450 adantll ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → w ∈ b
452 iffalse ⊢ ¬ 1 st ⁡ w = 1 st ⁡ c → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙ = if w ∈ d 1 ˙ 0 ˙
453 452 adantl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙ = if w ∈ d 1 ˙ 0 ˙
454 setsres ⊢ d ∈ V → d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c = d ↾ V ∖ 1 st ⁡ c
455 454 eleq2d ⊢ d ∈ V → 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d ↾ V ∖ 1 st ⁡ c
456 426 455 mp1i ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d ↾ V ∖ 1 st ⁡ c
457 fvex ⊢ 1 st ⁡ w ∈ V
458 457 a1i ⊢ ¬ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w ∈ V
459 neqne ⊢ ¬ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w ≠ 1 st ⁡ c
460 eldifsn ⊢ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w ∈ V ∧ 1 st ⁡ w ≠ 1 st ⁡ c
461 458 459 460 sylanbrc ⊢ ¬ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w ∈ V ∖ 1 st ⁡ c
462 fvex ⊢ 2 nd ⁡ w ∈ V
463 462 opres ⊢ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
464 463 adantl ⊢ w ∈ N × N ∧ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
465 1st2nd2 ⊢ w ∈ N × N → w = 1 st ⁡ w 2 nd ⁡ w
466 465 eleq1d ⊢ w ∈ N × N → w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
467 466 adantr ⊢ w ∈ N × N ∧ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
468 464 467 bitr4d ⊢ w ∈ N × N ∧ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c ↔ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
469 403 461 468 syl2an ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c ↾ V ∖ 1 st ⁡ c ↔ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
470 462 opres ⊢ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d ↾ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d
471 470 adantl ⊢ w ∈ N × N ∧ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d ↾ V ∖ 1 st ⁡ c ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d
472 465 eleq1d ⊢ w ∈ N × N → w ∈ d ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d
473 472 adantr ⊢ w ∈ N × N ∧ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → w ∈ d ↔ 1 st ⁡ w 2 nd ⁡ w ∈ d
474 471 473 bitr4d ⊢ w ∈ N × N ∧ 1 st ⁡ w ∈ V ∖ 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d ↾ V ∖ 1 st ⁡ c ↔ w ∈ d
475 403 461 474 syl2an ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → 1 st ⁡ w 2 nd ⁡ w ∈ d ↾ V ∖ 1 st ⁡ c ↔ w ∈ d
476 456 469 475 3bitr3rd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → w ∈ d ↔ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
477 476 ifbid ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → if w ∈ d 1 ˙ 0 ˙ = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
478 453 477 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙ = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
479 ifeq2 ⊢ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙
480 479 eqeq1d ⊢ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙ ↔ if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙ = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
481 478 480 syl5ibrcom ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
482 451 481 embantd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c ∧ ¬ 1 st ⁡ w = 1 st ⁡ c → w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
483 442 482 pm2.61dan ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c → w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
484 fveqeq2 ⊢ e = w → 1 st ⁡ e = 1 st ⁡ c ↔ 1 st ⁡ w = 1 st ⁡ c
485 equequ1 ⊢ e = w → e = c ↔ w = c
486 485 ifbid ⊢ e = w → if e = c 1 ˙ 0 ˙ = if w = c 1 ˙ 0 ˙
487 fveq2 ⊢ e = w → a ⁡ e = a ⁡ w
488 484 486 487 ifbieq12d ⊢ e = w → if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w
489 eqid ⊢ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e
490 165 162 ifex ⊢ if w = c 1 ˙ 0 ˙ ∈ V
491 fvex ⊢ a ⁡ w ∈ V
492 490 491 ifex ⊢ if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w ∈ V
493 488 489 492 fvmpt ⊢ w ∈ N × N → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w
494 493 eqeq1d ⊢ w ∈ N × N → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙ ↔ if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
495 403 494 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙ ↔ if 1 st ⁡ w = 1 st ⁡ c if w = c 1 ˙ 0 ˙ a ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
496 483 495 sylibrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ w ∈ b ∪ c → w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
497 496 ralimdva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → ∀ w ∈ b ∪ c w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
498 396 497 biimtrid ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
499 498 impr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
500 499 3adantr1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
501 348 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ B
502 simpr2 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → d ∈ N N
503 502 409 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → d : N ⟶ N
504 124 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → 1 st ⁡ c ∈ N
505 413 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → 2 nd ⁡ c ∈ N
506 502 503 504 505 415 syl211anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → d sSet 1 st ⁡ c 2 nd ⁡ c : N ⟶ N
507 158 158 elmapd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → d sSet 1 st ⁡ c 2 nd ⁡ c ∈ N N ↔ d sSet 1 st ⁡ c 2 nd ⁡ c : N ⟶ N
508 507 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → d sSet 1 st ⁡ c 2 nd ⁡ c ∈ N N ↔ d sSet 1 st ⁡ c 2 nd ⁡ c : N ⟶ N
509 506 508 mpbird ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → d sSet 1 st ⁡ c 2 nd ⁡ c ∈ N N
510 simpr1 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → b ∪ c ∈ Y
511 raleq ⊢ x = b ∪ c → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙
512 511 imbi1d ⊢ x = b ∪ c → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
513 512 2ralbidv ⊢ x = b ∪ c → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
514 513 15 elab2g ⊢ b ∪ c ∈ Y → b ∪ c ∈ Y ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
515 514 ibi ⊢ b ∪ c ∈ Y → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
516 510 515 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
517 fveq1 ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → y ⁡ w = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w
518 517 eqeq1d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙
519 518 ralbidv ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙
520 fveqeq2 ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → D ⁡ y = 0 ˙ ↔ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙
521 519 520 imbi12d ⊢ y = e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e → ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙
522 eleq2 ⊢ z = d sSet 1 st ⁡ c 2 nd ⁡ c → w ∈ z ↔ w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c
523 522 ifbid ⊢ z = d sSet 1 st ⁡ c 2 nd ⁡ c → if w ∈ z 1 ˙ 0 ˙ = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
524 523 eqeq2d ⊢ z = d sSet 1 st ⁡ c 2 nd ⁡ c → e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
525 524 ralbidv ⊢ z = d sSet 1 st ⁡ c 2 nd ⁡ c → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙
526 525 imbi1d ⊢ z = d sSet 1 st ⁡ c 2 nd ⁡ c → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙
527 521 526 rspc2va ⊢ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ∈ B ∧ d sSet 1 st ⁡ c 2 nd ⁡ c ∈ N N ∧ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙
528 501 509 516 527 syl21anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d sSet 1 st ⁡ c 2 nd ⁡ c 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙
529 500 528 mpd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = 0 ˙
530 529 oveq2d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙
531 118 unssad ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → b ⊆ N × N
532 531 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → b ⊆ N × N
533 simpr3 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙
534 ssel2 ⊢ b ⊆ N × N ∧ w ∈ b → w ∈ N × N
535 534 adantr ⊢ b ⊆ N × N ∧ w ∈ b ∧ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → w ∈ N × N
536 elequ1 ⊢ e = w → e ∈ d ↔ w ∈ d
537 536 ifbid ⊢ e = w → if e ∈ d 1 ˙ 0 ˙ = if w ∈ d 1 ˙ 0 ˙
538 485 537 487 ifbieq12d ⊢ e = w → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w
539 eqid ⊢ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e
540 165 162 ifex ⊢ if w ∈ d 1 ˙ 0 ˙ ∈ V
541 540 491 ifex ⊢ if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w ∈ V
542 538 539 541 fvmpt ⊢ w ∈ N × N → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w
543 535 542 syl ⊢ b ⊆ N × N ∧ w ∈ b ∧ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w
544 ifeq2 ⊢ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w = if w = c if w ∈ d 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙
545 544 adantl ⊢ b ⊆ N × N ∧ w ∈ b ∧ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w = if w = c if w ∈ d 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙
546 ifid ⊢ if w = c if w ∈ d 1 ˙ 0 ˙ if w ∈ d 1 ˙ 0 ˙ = if w ∈ d 1 ˙ 0 ˙
547 545 546 eqtrdi ⊢ b ⊆ N × N ∧ w ∈ b ∧ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → if w = c if w ∈ d 1 ˙ 0 ˙ a ⁡ w = if w ∈ d 1 ˙ 0 ˙
548 543 547 eqtrd ⊢ b ⊆ N × N ∧ w ∈ b ∧ a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
549 548 ex ⊢ b ⊆ N × N ∧ w ∈ b → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
550 549 ralimdva ⊢ b ⊆ N × N → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
551 532 533 550 sylc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
552 142 291 eqtrd ⊢ e = c → if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = if c ∈ d 1 ˙ 0 ˙
553 165 162 ifex ⊢ if c ∈ d 1 ˙ 0 ˙ ∈ V
554 552 539 553 fvmpt ⊢ c ∈ N × N → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c = if c ∈ d 1 ˙ 0 ˙
555 122 554 syl ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c = if c ∈ d 1 ˙ 0 ˙
556 555 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c = if c ∈ d 1 ˙ 0 ˙
557 fveq2 ⊢ w = c → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c
558 elequ1 ⊢ w = c → w ∈ d ↔ c ∈ d
559 558 ifbid ⊢ w = c → if w ∈ d 1 ˙ 0 ˙ = if c ∈ d 1 ˙ 0 ˙
560 557 559 eqeq12d ⊢ w = c → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c = if c ∈ d 1 ˙ 0 ˙
561 560 ralunsn ⊢ c ∈ V → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ ∀ w ∈ b e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ ∧ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c = if c ∈ d 1 ˙ 0 ˙
562 561 elv ⊢ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ ∀ w ∈ b e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ ∧ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ c = if c ∈ d 1 ˙ 0 ˙
563 551 556 562 sylanbrc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
564 223 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ B
565 fveq1 ⊢ y = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → y ⁡ w = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w
566 565 eqeq1d ⊢ y = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙
567 566 ralbidv ⊢ y = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙
568 fveqeq2 ⊢ y = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → D ⁡ y = 0 ˙ ↔ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
569 567 568 imbi12d ⊢ y = e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e → ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
570 elequ2 ⊢ z = d → w ∈ z ↔ w ∈ d
571 570 ifbid ⊢ z = d → if w ∈ z 1 ˙ 0 ˙ = if w ∈ d 1 ˙ 0 ˙
572 571 eqeq2d ⊢ z = d → e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
573 572 ralbidv ⊢ z = d → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙
574 573 imbi1d ⊢ z = d → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙ ↔ ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
575 569 574 rspc2va ⊢ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ∈ B ∧ d ∈ N N ∧ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b ∪ c y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
576 564 502 516 575 syl21anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → ∀ w ∈ b ∪ c e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
577 563 576 mpd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
578 530 577 oveq12d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙ + ˙ 0 ˙
579 308 oveq1d ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙ + ˙ 0 ˙ = 0 ˙ + ˙ 0 ˙
580 3 6 4 grplid ⊢ R ∈ Grp ∧ 0 ˙ ∈ K → 0 ˙ + ˙ 0 ˙ = 0 ˙
581 115 133 580 syl2anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → 0 ˙ + ˙ 0 ˙ = 0 ˙
582 579 581 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙ + ˙ 0 ˙ = 0 ˙
583 582 adantr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ 0 ˙ + ˙ 0 ˙ = 0 ˙
584 578 583 eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ a ∈ B ∧ b ∪ c ∈ Y ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
585 104 105 106 392 393 394 584 syl33anc ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → a ⁡ c - R if c ∈ d 1 ˙ 0 ˙ · ˙ D ⁡ e ∈ N × N ⟼ if 1 st ⁡ e = 1 st ⁡ c if e = c 1 ˙ 0 ˙ a ⁡ e + ˙ D ⁡ e ∈ N × N ⟼ if e = c if e ∈ d 1 ˙ 0 ˙ a ⁡ e = 0 ˙
586 288 391 585 3eqtrd ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N ∧ ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
587 586 expr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y ∧ a ∈ B ∧ d ∈ N N → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
588 587 ralrimivva ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y → ∀ a ∈ B ∀ d ∈ N N ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
589 fveq1 ⊢ a = y → a ⁡ w = y ⁡ w
590 589 eqeq1d ⊢ a = y → a ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ y ⁡ w = if w ∈ d 1 ˙ 0 ˙
591 590 ralbidv ⊢ a = y → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ ∀ w ∈ b y ⁡ w = if w ∈ d 1 ˙ 0 ˙
592 fveqeq2 ⊢ a = y → D ⁡ a = 0 ˙ ↔ D ⁡ y = 0 ˙
593 591 592 imbi12d ⊢ a = y → ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ a = 0 ˙ ↔ ∀ w ∈ b y ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
594 elequ2 ⊢ d = z → w ∈ d ↔ w ∈ z
595 594 ifbid ⊢ d = z → if w ∈ d 1 ˙ 0 ˙ = if w ∈ z 1 ˙ 0 ˙
596 595 eqeq2d ⊢ d = z → y ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ y ⁡ w = if w ∈ z 1 ˙ 0 ˙
597 596 ralbidv ⊢ d = z → ∀ w ∈ b y ⁡ w = if w ∈ d 1 ˙ 0 ˙ ↔ ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙
598 597 imbi1d ⊢ d = z → ∀ w ∈ b y ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
599 593 598 cbvral2vw ⊢ ∀ a ∈ B ∀ d ∈ N N ∀ w ∈ b a ⁡ w = if w ∈ d 1 ˙ 0 ˙ → D ⁡ a = 0 ˙ ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
600 588 599 sylib ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
601 vex ⊢ b ∈ V
602 raleq ⊢ x = b → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙
603 602 imbi1d ⊢ x = b → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
604 603 2ralbidv ⊢ x = b → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
605 601 604 15 elab2 ⊢ b ∈ Y ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ b y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
606 600 605 sylibr ⊢ φ ∧ b ∪ c ⊆ N × N ∧ b ∪ c ∈ Y → b ∈ Y
607 606 3expia ⊢ φ ∧ b ∪ c ⊆ N × N → b ∪ c ∈ Y → b ∈ Y
608 607 con3d ⊢ φ ∧ b ∪ c ⊆ N × N → ¬ b ∈ Y → ¬ b ∪ c ∈ Y
609 608 3adant3 ⊢ φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y → ¬ b ∪ c ∈ Y
610 609 a1i ⊢ b ∈ Fin ∧ ¬ c ∈ b → φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y → ¬ b ∪ c ∈ Y
611 610 a2d ⊢ b ∈ Fin ∧ ¬ c ∈ b → φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y → φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∪ c ∈ Y
612 103 611 syl5 ⊢ b ∈ Fin ∧ ¬ c ∈ b → φ ∧ b ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∈ Y → φ ∧ b ∪ c ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ b ∪ c ∈ Y
613 82 87 92 97 98 612 findcard2s ⊢ N × N ∈ Fin → φ ∧ N × N ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ N × N ∈ Y
614 77 613 mpcom ⊢ φ ∧ N × N ⊆ N × N ∧ ¬ ∅ ∈ Y → ¬ N × N ∈ Y
615 614 3exp ⊢ φ → N × N ⊆ N × N → ¬ ∅ ∈ Y → ¬ N × N ∈ Y
616 76 615 mpi ⊢ φ → ¬ ∅ ∈ Y → ¬ N × N ∈ Y
617 75 616 mt4d ⊢ φ → ∅ ∈ Y
618 617 adantr ⊢ φ ∧ a ∈ B → ∅ ∈ Y
619 0ex ⊢ ∅ ∈ V
620 raleq ⊢ x = ∅ → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙
621 620 imbi1d ⊢ x = ∅ → ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
622 621 2ralbidv ⊢ x = ∅ → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ x y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
623 619 622 15 elab2 ⊢ ∅ ∈ Y ↔ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
624 618 623 sylib ⊢ φ ∧ a ∈ B → ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙
625 fveq1 ⊢ y = a → y ⁡ w = a ⁡ w
626 625 eqeq1d ⊢ y = a → y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ a ⁡ w = if w ∈ z 1 ˙ 0 ˙
627 626 ralbidv ⊢ y = a → ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ ∅ a ⁡ w = if w ∈ z 1 ˙ 0 ˙
628 fveqeq2 ⊢ y = a → D ⁡ y = 0 ˙ ↔ D ⁡ a = 0 ˙
629 627 628 imbi12d ⊢ y = a → ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ ↔ ∀ w ∈ ∅ a ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
630 eleq2 ⊢ z = I ↾ N → w ∈ z ↔ w ∈ I ↾ N
631 630 ifbid ⊢ z = I ↾ N → if w ∈ z 1 ˙ 0 ˙ = if w ∈ I ↾ N 1 ˙ 0 ˙
632 631 eqeq2d ⊢ z = I ↾ N → a ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ a ⁡ w = if w ∈ I ↾ N 1 ˙ 0 ˙
633 632 ralbidv ⊢ z = I ↾ N → ∀ w ∈ ∅ a ⁡ w = if w ∈ z 1 ˙ 0 ˙ ↔ ∀ w ∈ ∅ a ⁡ w = if w ∈ I ↾ N 1 ˙ 0 ˙
634 633 imbi1d ⊢ z = I ↾ N → ∀ w ∈ ∅ a ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ a = 0 ˙ ↔ ∀ w ∈ ∅ a ⁡ w = if w ∈ I ↾ N 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
635 629 634 rspc2va ⊢ a ∈ B ∧ I ↾ N ∈ N N ∧ ∀ y ∈ B ∀ z ∈ N N ∀ w ∈ ∅ y ⁡ w = if w ∈ z 1 ˙ 0 ˙ → D ⁡ y = 0 ˙ → ∀ w ∈ ∅ a ⁡ w = if w ∈ I ↾ N 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
636 17 23 624 635 syl21anc ⊢ φ ∧ a ∈ B → ∀ w ∈ ∅ a ⁡ w = if w ∈ I ↾ N 1 ˙ 0 ˙ → D ⁡ a = 0 ˙
637 16 636 mpi ⊢ φ ∧ a ∈ B → D ⁡ a = 0 ˙
638 637 mpteq2dva ⊢ φ → a ∈ B ⟼ D ⁡ a = a ∈ B ⟼ 0 ˙
639 10 feqmptd ⊢ φ → D = a ∈ B ⟼ D ⁡ a
640 fconstmpt ⊢ B × 0 ˙ = a ∈ B ⟼ 0 ˙
641 640 a1i ⊢ φ → B × 0 ˙ = a ∈ B ⟼ 0 ˙
642 638 639 641 3eqtr4d ⊢ φ → D = B × 0 ˙