Theorem hbrdg 2974

Description: Bound-variable hypothesis builder for the recursive definition generator.

Hypotheses

Ref	Expression
hbrdg.1	|- (y e. F -> A.x y e. F)
hbrdg.2	|- (y e. A -> A.x y e. A)

Assertion

Ref	Expression
hbrdg	|- (y e. rec(F, A) -> A.x y e. rec(F, A))

Distinct variable group(s):   y,F   y,A   x,y

Proof of Theorem hbrdg

Step	Hyp	Ref	Expression
1		ax-17 925	. . . . 5 |- (w e. On -> A.x w e. On)
2		ax-17 925	. . . . . 6 |- (f Fn w -> A.x f Fn w)
3		ax-17 925	. . . . . . 7 |- (v e. w -> A.x v e. w)
4		ax-17 925	. . . . . . . 8 |- (y e. (f` v) -> A.x y e. (f` v))
5		ax-17 925	. . . . . . . . . . . 12 |- (g = (/) -> A.x g = (/))
6		ax-17 925	. . . . . . . . . . . . 13 |- (y e. z -> A.x y e. z)
7		hbrdg.2	. . . . . . . . . . . . 13 |- (y e. A -> A.x y e. A)
8	6, 7	hbeq 1171	. . . . . . . . . . . 12 |- (z = A -> A.x z = A)
9	5, 8	hban 704	. . . . . . . . . . 11 |- ((g = (/) /\ z = A) -> A.x(g = (/) /\ z = A))
10		ax-17 925	. . . . . . . . . . . 12 |- (-. (g = (/) \/ Lim dom g) -> A.x -. (g = (/) \/ Lim dom g))
11		hbrdg.1	. . . . . . . . . . . . . 14 |- (y e. F -> A.x y e. F)
12		ax-17 925	. . . . . . . . . . . . . 14 |- (y e. (g` U.dom g) -> A.x y e. (g` U.dom g))
13	11, 12	hbfv 2837	. . . . . . . . . . . . 13 |- (y e. (F` (g` U.dom g)) -> A.x y e. (F` (g` U.dom g)))
14	6, 13	hbeq 1171	. . . . . . . . . . . 12 |- (z = (F` (g` U.dom g)) -> A.x z = (F` (g` U.dom g)))
15	10, 14	hban 704	. . . . . . . . . . 11 |- ((-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) -> A.x(-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))))
16		ax-17 925	. . . . . . . . . . 11 |- ((Lim dom g /\ z = U.ran g) -> A.x(Lim dom g /\ z = U.ran g))
17	9, 15, 16	hb3or 706	. . . . . . . . . 10 |- (((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g)) -> A.x((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g)))
18	17	hbopab 2111	. . . . . . . . 9 |- (y e. {<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))} -> A.x y e. {<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))})
19		ax-17 925	. . . . . . . . 9 |- (y e. (f |` v) -> A.x y e. (f |` v))
20	18, 19	hbfv 2837	. . . . . . . 8 |- (y e. ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)) -> A.x y e. ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))
21	4, 20	hbeq 1171	. . . . . . 7 |- ((f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)) -> A.x(f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))
22	3, 21	hbral 1236	. . . . . 6 |- (A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)) -> A.xA.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))
23	2, 22	hban 704	. . . . 5 |- ((f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v))) -> A.x(f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v))))
24	1, 23	hbrex 1238	. . . 4 |- (E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v))) -> A.xE.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v))))
25	24	hbab 1096	. . 3 |- (y e. {f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))} -> A.x y e. {f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))})
26	25	hbuni 1925	. 2 |- (y e. U.{f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))} -> A.x y e. U.{f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))})
27		df-rdg 2970	. . 3 |- rec(F, A) = U.{f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))}
28	27	eleq2i 1153	. 2 |- (y e. rec(F, A) <-> y e. U.{f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))})
29	28	bial 695	. 2 |- (A.x y e. rec(F, A) <-> A.x y e. U.{f | E.w e. On (f Fn w /\ A.v e. w (f` v) = ({<.g, z>. | ((g = (/) /\ z = A) \/ (-. (g = (/) \/ Lim dom g) /\ z = (F` (g` U.dom g))) \/ (Lim dom g /\ z = U.ran g))}` (f |` v)))})
30	26, 28, 29	3imtr4 192	1 |- (y e. rec(F, A) -> A.x y e. rec(F, A))