Metamath Proof Explorer


Theorem dfrdg4

Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfrdg4 rec F A = 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼

Proof

Step Hyp Ref Expression
1 dfrdg3 rec F A = f | x On f Fn x y x f y = if y = if A V A if Lim y f y F f y
2 an12 x On f Fn x y x f y = if y = if A V A if Lim y f y F f y f Fn x x On y x f y = if y = if A V A if Lim y f y F f y
3 df-fn f Fn x Fun f dom f = x
4 ancom Fun f dom f = x dom f = x Fun f
5 eqcom dom f = x x = dom f
6 5 anbi1i dom f = x Fun f x = dom f Fun f
7 3 4 6 3bitri f Fn x x = dom f Fun f
8 7 anbi1i f Fn x x On y x f y = if y = if A V A if Lim y f y F f y x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y
9 anass x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y
10 2 8 9 3bitri x On f Fn x y x f y = if y = if A V A if Lim y f y F f y x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y
11 10 exbii x x On f Fn x y x f y = if y = if A V A if Lim y f y F f y x x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y
12 vex f V
13 12 dmex dom f V
14 eleq1 x = dom f x On dom f On
15 raleq x = dom f y x f y = if y = if A V A if Lim y f y F f y y dom f f y = if y = if A V A if Lim y f y F f y
16 14 15 anbi12d x = dom f x On y x f y = if y = if A V A if Lim y f y F f y dom f On y dom f f y = if y = if A V A if Lim y f y F f y
17 16 anbi2d x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
18 13 17 ceqsexv x x = dom f Fun f x On y x f y = if y = if A V A if Lim y f y F f y Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
19 11 18 bitri x x On f Fn x y x f y = if y = if A V A if Lim y f y F f y Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
20 df-rex x On f Fn x y x f y = if y = if A V A if Lim y f y F f y x x On f Fn x y x f y = if y = if A V A if Lim y f y F f y
21 eldif f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼
22 elin f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On f 𝖥𝗎𝗇𝗌 f 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On
23 12 elfuns f 𝖥𝗎𝗇𝗌 Fun f
24 12 elima f 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On x On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f
25 df-rex x On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f x x On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f
26 vex x V
27 26 12 brcnv x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f f 𝖣𝗈𝗆𝖺𝗂𝗇 x
28 12 26 brdomain f 𝖣𝗈𝗆𝖺𝗂𝗇 x x = dom f
29 27 28 bitri x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f x = dom f
30 29 anbi1ci x On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f x = dom f x On
31 30 exbii x x On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f x x = dom f x On
32 13 14 ceqsexv x x = dom f x On dom f On
33 31 32 bitri x x On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f dom f On
34 24 25 33 3bitri f 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom f On
35 23 34 anbi12i f 𝖥𝗎𝗇𝗌 f 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On Fun f dom f On
36 22 35 bitri f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On Fun f dom f On
37 36 anbi1i f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 Fun f dom f On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼
38 brdif f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 y ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y
39 vex y V
40 12 39 brco f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 y x f 𝖣𝗈𝗆𝖺𝗂𝗇 x x E -1 y
41 28 anbi1i f 𝖣𝗈𝗆𝖺𝗂𝗇 x x E -1 y x = dom f x E -1 y
42 41 exbii x f 𝖣𝗈𝗆𝖺𝗂𝗇 x x E -1 y x x = dom f x E -1 y
43 breq1 x = dom f x E -1 y dom f E -1 y
44 13 43 ceqsexv x x = dom f x E -1 y dom f E -1 y
45 42 44 bitri x f 𝖣𝗈𝗆𝖺𝗂𝗇 x x E -1 y dom f E -1 y
46 13 39 brcnv dom f E -1 y y E dom f
47 13 epeli y E dom f y dom f
48 46 47 bitri dom f E -1 y y dom f
49 40 45 48 3bitri f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 y y dom f
50 49 anbi1i f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 y ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y y dom f ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y
51 38 50 bitri f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y y dom f ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y
52 onelon dom f On y dom f y On
53 52 3adant1 Fun f dom f On y dom f y On
54 brun f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x f y V × × A x f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x
55 brxp f y V × × A x f y V × x A
56 opelxp f y V × f V y
57 12 56 mpbiran f y V × y
58 velsn y y =
59 57 58 bitri f y V × y =
60 velsn x A x = A
61 59 60 anbi12i f y V × x A y = x = A
62 55 61 bitri f y V × × A x y = x = A
63 brun f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 x f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x
64 26 brresi f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 x f y V × 𝖫𝗂𝗆𝗂𝗍𝗌 f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 x
65 opelxp f y V × 𝖫𝗂𝗆𝗂𝗍𝗌 f V y 𝖫𝗂𝗆𝗂𝗍𝗌
66 12 65 mpbiran f y V × 𝖫𝗂𝗆𝗂𝗍𝗌 y 𝖫𝗂𝗆𝗂𝗍𝗌
67 39 ellimits y 𝖫𝗂𝗆𝗂𝗍𝗌 Lim y
68 66 67 bitri f y V × 𝖫𝗂𝗆𝗂𝗍𝗌 Lim y
69 opex f y V
70 69 26 brco f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 x z f y 𝖨𝗆𝗀 z z 𝖡𝗂𝗀𝖼𝗎𝗉 x
71 vex z V
72 12 39 71 brimg f y 𝖨𝗆𝗀 z z = f y
73 26 brbigcup z 𝖡𝗂𝗀𝖼𝗎𝗉 x z = x
74 72 73 anbi12i f y 𝖨𝗆𝗀 z z 𝖡𝗂𝗀𝖼𝗎𝗉 x z = f y z = x
75 74 exbii z f y 𝖨𝗆𝗀 z z 𝖡𝗂𝗀𝖼𝗎𝗉 x z z = f y z = x
76 12 imaex f y V
77 unieq z = f y z = f y
78 77 eqeq1d z = f y z = x f y = x
79 76 78 ceqsexv z z = f y z = x f y = x
80 eqcom f y = x x = f y
81 79 80 bitri z z = f y z = x x = f y
82 70 75 81 3bitri f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 x x = f y
83 68 82 anbi12i f y V × 𝖫𝗂𝗆𝗂𝗍𝗌 f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 x Lim y x = f y
84 64 83 bitri f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 x Lim y x = f y
85 26 brresi f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x f y V × ran 𝖲𝗎𝖼𝖼 f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x
86 opelxp f y V × ran 𝖲𝗎𝖼𝖼 f V y ran 𝖲𝗎𝖼𝖼
87 12 86 mpbiran f y V × ran 𝖲𝗎𝖼𝖼 y ran 𝖲𝗎𝖼𝖼
88 39 elrn y ran 𝖲𝗎𝖼𝖼 z z 𝖲𝗎𝖼𝖼 y
89 71 39 brsuccf z 𝖲𝗎𝖼𝖼 y y = suc z
90 89 exbii z z 𝖲𝗎𝖼𝖼 y z y = suc z
91 87 88 90 3bitri f y V × ran 𝖲𝗎𝖼𝖼 z y = suc z
92 69 26 brco f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x a f y 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x
93 vex a V
94 69 93 brco f y 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a z f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z z 𝖠𝗉𝗉𝗅𝗒 a
95 12 39 71 brpprod3a f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z a b z = a b f I a y 𝖡𝗂𝗀𝖼𝗎𝗉 b
96 3anrot z = a b f I a y 𝖡𝗂𝗀𝖼𝗎𝗉 b f I a y 𝖡𝗂𝗀𝖼𝗎𝗉 b z = a b
97 93 ideq f I a f = a
98 equcom f = a a = f
99 97 98 bitri f I a a = f
100 vex b V
101 100 brbigcup y 𝖡𝗂𝗀𝖼𝗎𝗉 b y = b
102 eqcom y = b b = y
103 101 102 bitri y 𝖡𝗂𝗀𝖼𝗎𝗉 b b = y
104 biid z = a b z = a b
105 99 103 104 3anbi123i f I a y 𝖡𝗂𝗀𝖼𝗎𝗉 b z = a b a = f b = y z = a b
106 96 105 bitri z = a b f I a y 𝖡𝗂𝗀𝖼𝗎𝗉 b a = f b = y z = a b
107 106 2exbii a b z = a b f I a y 𝖡𝗂𝗀𝖼𝗎𝗉 b a b a = f b = y z = a b
108 vuniex y V
109 opeq1 a = f a b = f b
110 109 eqeq2d a = f z = a b z = f b
111 opeq2 b = y f b = f y
112 111 eqeq2d b = y z = f b z = f y
113 12 108 110 112 ceqsex2v a b a = f b = y z = a b z = f y
114 95 107 113 3bitri f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z z = f y
115 114 anbi1i f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z z 𝖠𝗉𝗉𝗅𝗒 a z = f y z 𝖠𝗉𝗉𝗅𝗒 a
116 115 exbii z f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z z 𝖠𝗉𝗉𝗅𝗒 a z z = f y z 𝖠𝗉𝗉𝗅𝗒 a
117 opex f y V
118 breq1 z = f y z 𝖠𝗉𝗉𝗅𝗒 a f y 𝖠𝗉𝗉𝗅𝗒 a
119 117 118 ceqsexv z z = f y z 𝖠𝗉𝗉𝗅𝗒 a f y 𝖠𝗉𝗉𝗅𝗒 a
120 12 108 93 brapply f y 𝖠𝗉𝗉𝗅𝗒 a a = f y
121 119 120 bitri z z = f y z 𝖠𝗉𝗉𝗅𝗒 a a = f y
122 94 116 121 3bitri f y 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a a = f y
123 93 26 brfullfun a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x x = F a
124 122 123 anbi12i f y 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x a = f y x = F a
125 124 exbii a f y 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x a a = f y x = F a
126 fvex f y V
127 fveq2 a = f y F a = F f y
128 127 eqeq2d a = f y x = F a x = F f y
129 126 128 ceqsexv a a = f y x = F a x = F f y
130 92 125 129 3bitri f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x x = F f y
131 91 130 anbi12i f y V × ran 𝖲𝗎𝖼𝖼 f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x z y = suc z x = F f y
132 85 131 bitri f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x z y = suc z x = F f y
133 84 132 orbi12i f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 x f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x Lim y x = f y z y = suc z x = F f y
134 63 133 bitri f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x Lim y x = f y z y = suc z x = F f y
135 62 134 orbi12i f y V × × A x f y 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x y = x = A Lim y x = f y z y = suc z x = F f y
136 54 135 bitri f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x y = x = A Lim y x = f y z y = suc z x = F f y
137 onzsl y On y = z On y = suc z y V Lim y
138 nlim0 ¬ Lim
139 limeq y = Lim y Lim
140 138 139 mtbiri y = ¬ Lim y
141 140 intnanrd y = ¬ Lim y x = f y
142 nsuceq0 suc z
143 neeq2 y = suc z y suc z
144 142 143 mpbiri y = suc z y
145 144 necomd y = y suc z
146 145 neneqd y = ¬ y = suc z
147 146 nexdv y = ¬ z y = suc z
148 147 intnanrd y = ¬ z y = suc z x = F f y
149 ioran ¬ Lim y x = f y z y = suc z x = F f y ¬ Lim y x = f y ¬ z y = suc z x = F f y
150 141 148 149 sylanbrc y = ¬ Lim y x = f y z y = suc z x = F f y
151 orel2 ¬ Lim y x = f y z y = suc z x = F f y y = x = A Lim y x = f y z y = suc z x = F f y y = x = A
152 150 151 syl y = y = x = A Lim y x = f y z y = suc z x = F f y y = x = A
153 iftrue y = if y = if A V A if Lim y f y F f y = if A V A
154 unisnif A = if A V A
155 153 154 eqtr4di y = if y = if A V A if Lim y f y F f y = A
156 155 eqeq2d y = x = if y = if A V A if Lim y f y F f y x = A
157 156 biimprd y = x = A x = if y = if A V A if Lim y f y F f y
158 157 adantld y = y = x = A x = if y = if A V A if Lim y f y F f y
159 152 158 syld y = y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
160 156 biimpd y = x = if y = if A V A if Lim y f y F f y x = A
161 160 anc2li y = x = if y = if A V A if Lim y f y F f y y = x = A
162 orc y = x = A y = x = A Lim y x = f y z y = suc z x = F f y
163 161 162 syl6 y = x = if y = if A V A if Lim y f y F f y y = x = A Lim y x = f y z y = suc z x = F f y
164 159 163 impbid y = y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
165 neeq1 y = suc z y suc z
166 142 165 mpbiri y = suc z y
167 166 neneqd y = suc z ¬ y =
168 167 intnanrd y = suc z ¬ y = x = A
169 168 rexlimivw z On y = suc z ¬ y = x = A
170 orel1 ¬ y = x = A y = x = A Lim y x = f y z y = suc z x = F f y Lim y x = f y z y = suc z x = F f y
171 169 170 syl z On y = suc z y = x = A Lim y x = f y z y = suc z x = F f y Lim y x = f y z y = suc z x = F f y
172 nlimsucg z V ¬ Lim suc z
173 172 elv ¬ Lim suc z
174 limeq y = suc z Lim y Lim suc z
175 173 174 mtbiri y = suc z ¬ Lim y
176 175 rexlimivw z On y = suc z ¬ Lim y
177 176 intnanrd z On y = suc z ¬ Lim y x = f y
178 orel1 ¬ Lim y x = f y Lim y x = f y z y = suc z x = F f y z y = suc z x = F f y
179 177 178 syl z On y = suc z Lim y x = f y z y = suc z x = F f y z y = suc z x = F f y
180 142 neii ¬ suc z =
181 180 iffalsei if suc z = if A V A if Lim suc z f y F f suc z = if Lim suc z f y F f suc z
182 iffalse ¬ Lim suc z if Lim suc z f y F f suc z = F f suc z
183 71 172 182 mp2b if Lim suc z f y F f suc z = F f suc z
184 181 183 eqtri if suc z = if A V A if Lim suc z f y F f suc z = F f suc z
185 eqeq1 y = suc z y = suc z =
186 unieq y = suc z y = suc z
187 186 fveq2d y = suc z f y = f suc z
188 187 fveq2d y = suc z F f y = F f suc z
189 174 188 ifbieq2d y = suc z if Lim y f y F f y = if Lim suc z f y F f suc z
190 185 189 ifbieq2d y = suc z if y = if A V A if Lim y f y F f y = if suc z = if A V A if Lim suc z f y F f suc z
191 184 190 188 3eqtr4a y = suc z if y = if A V A if Lim y f y F f y = F f y
192 191 rexlimivw z On y = suc z if y = if A V A if Lim y f y F f y = F f y
193 192 eqeq2d z On y = suc z x = if y = if A V A if Lim y f y F f y x = F f y
194 193 biimprd z On y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
195 194 adantld z On y = suc z z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
196 171 179 195 3syld z On y = suc z y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
197 rexex z On y = suc z z y = suc z
198 193 biimpd z On y = suc z x = if y = if A V A if Lim y f y F f y x = F f y
199 olc z y = suc z x = F f y Lim y x = f y z y = suc z x = F f y
200 199 olcd z y = suc z x = F f y y = x = A Lim y x = f y z y = suc z x = F f y
201 197 198 200 syl6an z On y = suc z x = if y = if A V A if Lim y f y F f y y = x = A Lim y x = f y z y = suc z x = F f y
202 196 201 impbid z On y = suc z y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
203 140 con2i Lim y ¬ y =
204 203 intnanrd Lim y ¬ y = x = A
205 204 170 syl Lim y y = x = A Lim y x = f y z y = suc z x = F f y Lim y x = f y z y = suc z x = F f y
206 175 exlimiv z y = suc z ¬ Lim y
207 206 con2i Lim y ¬ z y = suc z
208 207 intnanrd Lim y ¬ z y = suc z x = F f y
209 orel2 ¬ z y = suc z x = F f y Lim y x = f y z y = suc z x = F f y Lim y x = f y
210 208 209 syl Lim y Lim y x = f y z y = suc z x = F f y Lim y x = f y
211 203 iffalsed Lim y if y = if A V A if Lim y f y F f y = if Lim y f y F f y
212 iftrue Lim y if Lim y f y F f y = f y
213 211 212 eqtrd Lim y if y = if A V A if Lim y f y F f y = f y
214 213 eqeq2d Lim y x = if y = if A V A if Lim y f y F f y x = f y
215 214 biimprd Lim y x = f y x = if y = if A V A if Lim y f y F f y
216 215 adantld Lim y Lim y x = f y x = if y = if A V A if Lim y f y F f y
217 205 210 216 3syld Lim y y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
218 217 adantl y V Lim y y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
219 214 biimpd Lim y x = if y = if A V A if Lim y f y F f y x = f y
220 219 anc2li Lim y x = if y = if A V A if Lim y f y F f y Lim y x = f y
221 orc Lim y x = f y Lim y x = f y z y = suc z x = F f y
222 221 olcd Lim y x = f y y = x = A Lim y x = f y z y = suc z x = F f y
223 220 222 syl6 Lim y x = if y = if A V A if Lim y f y F f y y = x = A Lim y x = f y z y = suc z x = F f y
224 223 adantl y V Lim y x = if y = if A V A if Lim y f y F f y y = x = A Lim y x = f y z y = suc z x = F f y
225 218 224 impbid y V Lim y y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
226 164 202 225 3jaoi y = z On y = suc z y V Lim y y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
227 137 226 sylbi y On y = x = A Lim y x = f y z y = suc z x = F f y x = if y = if A V A if Lim y f y F f y
228 136 227 syl5bb y On f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x = if y = if A V A if Lim y f y F f y
229 53 228 syl Fun f dom f On y dom f f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x = if y = if A V A if Lim y f y F f y
230 26 69 brcnv x 𝖠𝗉𝗉𝗅𝗒 -1 f y f y 𝖠𝗉𝗉𝗅𝗒 x
231 12 39 26 brapply f y 𝖠𝗉𝗉𝗅𝗒 x x = f y
232 230 231 bitri x 𝖠𝗉𝗉𝗅𝗒 -1 f y x = f y
233 232 a1i Fun f dom f On y dom f x 𝖠𝗉𝗉𝗅𝗒 -1 f y x = f y
234 229 233 anbi12d Fun f dom f On y dom f f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x 𝖠𝗉𝗉𝗅𝗒 -1 f y x = if y = if A V A if Lim y f y F f y x = f y
235 234 biancomd Fun f dom f On y dom f f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x 𝖠𝗉𝗉𝗅𝗒 -1 f y x = f y x = if y = if A V A if Lim y f y F f y
236 235 exbidv Fun f dom f On y dom f x f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x 𝖠𝗉𝗉𝗅𝗒 -1 f y x x = f y x = if y = if A V A if Lim y f y F f y
237 df-br f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y f y 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼
238 69 elfix f y 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 f y 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 f y
239 69 69 brco f y 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 f y x f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x 𝖠𝗉𝗉𝗅𝗒 -1 f y
240 237 238 239 3bitri f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y x f y V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x x 𝖠𝗉𝗉𝗅𝗒 -1 f y
241 fvex f y V
242 241 eqvinc f y = if y = if A V A if Lim y f y F f y x x = f y x = if y = if A V A if Lim y f y F f y
243 236 240 242 3bitr4g Fun f dom f On y dom f f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y f y = if y = if A V A if Lim y f y F f y
244 243 notbid Fun f dom f On y dom f ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y ¬ f y = if y = if A V A if Lim y f y F f y
245 244 3expia Fun f dom f On y dom f ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y ¬ f y = if y = if A V A if Lim y f y F f y
246 245 pm5.32d Fun f dom f On y dom f ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y y dom f ¬ f y = if y = if A V A if Lim y f y F f y
247 annim y dom f ¬ f y = if y = if A V A if Lim y f y F f y ¬ y dom f f y = if y = if A V A if Lim y f y F f y
248 246 247 bitrdi Fun f dom f On y dom f ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y ¬ y dom f f y = if y = if A V A if Lim y f y F f y
249 51 248 syl5bb Fun f dom f On f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y ¬ y dom f f y = if y = if A V A if Lim y f y F f y
250 249 exbidv Fun f dom f On y f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y y ¬ y dom f f y = if y = if A V A if Lim y f y F f y
251 exnal y ¬ y dom f f y = if y = if A V A if Lim y f y F f y ¬ y y dom f f y = if y = if A V A if Lim y f y F f y
252 250 251 bitr2di Fun f dom f On ¬ y y dom f f y = if y = if A V A if Lim y f y F f y y f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y
253 12 eldm f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y f E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y
254 252 253 bitr4di Fun f dom f On ¬ y y dom f f y = if y = if A V A if Lim y f y F f y f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼
255 254 con1bid Fun f dom f On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y y dom f f y = if y = if A V A if Lim y f y F f y
256 df-ral y dom f f y = if y = if A V A if Lim y f y F f y y y dom f f y = if y = if A V A if Lim y f y F f y
257 255 256 bitr4di Fun f dom f On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 y dom f f y = if y = if A V A if Lim y f y F f y
258 257 pm5.32i Fun f dom f On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
259 anass Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
260 258 259 bitri Fun f dom f On ¬ f dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
261 21 37 260 3bitri f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 Fun f dom f On y dom f f y = if y = if A V A if Lim y f y F f y
262 19 20 261 3bitr4ri f 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 x On f Fn x y x f y = if y = if A V A if Lim y f y F f y
263 262 abbi2i 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 = f | x On f Fn x y x f y = if y = if A V A if Lim y f y F f y
264 263 unieqi 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼 = f | x On f Fn x y x f y = if y = if A V A if Lim y f y F f y
265 1 264 eqtr4i rec F A = 𝖥𝗎𝗇𝗌 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On dom E -1 𝖣𝗈𝗆𝖺𝗂𝗇 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 V × × A 𝖡𝗂𝗀𝖼𝗎𝗉 𝖨𝗆𝗀 V × 𝖫𝗂𝗆𝗂𝗍𝗌 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F 𝖠𝗉𝗉𝗅𝗒 pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 V × ran 𝖲𝗎𝖼𝖼