Theorem fictb 15371

Description: A set is countable iff its collection of finite intersections is countable.

Assertion

Ref	Expression
fictb	|- (A e. B -> (A ~<_ om <-> ( fi ` A) ~<_ om))

Proof of Theorem fictb

Step	Hyp	Ref	Expression
1		fiv 10212	. . . . . . 7 |- (A e. B -> ( fi ` A) = {t | E.r(r C_ A /\ r e. Fin /\ t = |^|r)})
2		sseq1 2637	. . . . . . . . . . . 12 |- (c = A -> (c C_ t <-> A C_ t))
3	2	anbi1d 679	. . . . . . . . . . 11 |- (c = A -> ((c C_ t /\ A.r e. t A.s e. t (r i^i s) e. t) <-> (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)))
4	3	abbidv 2008	. . . . . . . . . 10 |- (c = A -> {t | (c C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} = {t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)})
5	4	inteqd 3219	. . . . . . . . 9 |- (c = A -> |^|{t | (c C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} = |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)})
6		sseq2 2639	. . . . . . . . . . . 12 |- (c = A -> (r C_ c <-> r C_ A))
7	6	3anbi1d 1172	. . . . . . . . . . 11 |- (c = A -> ((r C_ c /\ r e. Fin /\ t = |^|r) <-> (r C_ A /\ r e. Fin /\ t = |^|r)))
8	7	exbidv 1657	. . . . . . . . . 10 |- (c = A -> (E.r(r C_ c /\ r e. Fin /\ t = |^|r) <-> E.r(r C_ A /\ r e. Fin /\ t = |^|r)))
9	8	abbidv 2008	. . . . . . . . 9 |- (c = A -> {t | E.r(r C_ c /\ r e. Fin /\ t = |^|r)} = {t | E.r(r C_ A /\ r e. Fin /\ t = |^|r)})
10	5, 9	eqeq12d 1899	. . . . . . . 8 |- (c = A -> (|^|{t | (c C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} = {t | E.r(r C_ c /\ r e. Fin /\ t = |^|r)} <-> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} = {t | E.r(r C_ A /\ r e. Fin /\ t = |^|r)}))
11		visset 2295	. . . . . . . . 9 |- c e. _V
12	11	abfii5 5655	. . . . . . . 8 |- |^|{t | (c C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} = {t | E.r(r C_ c /\ r e. Fin /\ t = |^|r)}
13	10, 12	vtoclg 2346	. . . . . . 7 |- (A e. B -> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} = {t | E.r(r C_ A /\ r e. Fin /\ t = |^|r)})
14	1, 13	eqtr4d 1928	. . . . . 6 |- (A e. B -> ( fi ` A) = |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)})
15	14	adantr 425	. . . . 5 |- ((A e. B /\ A ~<_ om) -> ( fi ` A) = |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)})
16		fvex 4689	. . . . . . 7 |- ( fi ` A) e. _V
17	15, 16	syl6eqelr 1980	. . . . . 6 |- ((A e. B /\ A ~<_ om) -> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} e. _V)
18		omex 5733	. . . . . . . . . 10 |- om e. _V
19		fvex 4689	. . . . . . . . . 10 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) e. _V
20	18, 19	iunex 4839	. . . . . . . . 9 |- U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) e. _V
21		sseq2 2639	. . . . . . . . . 10 |- (t = U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) -> (A C_ t <-> A C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
22		eleq2 1958	. . . . . . . . . . . 12 |- (t = U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) -> ((r i^i s) e. t <-> (r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
23	22	raleqbi1dv 2271	. . . . . . . . . . 11 |- (t = U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) -> (A.s e. t (r i^i s) e. t <-> A.s e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)(r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
24	23	raleqbi1dv 2271	. . . . . . . . . 10 |- (t = U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) -> (A.r e. t A.s e. t (r i^i s) e. t <-> A.r e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)A.s e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)(r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
25	21, 24	anbi12d 690	. . . . . . . . 9 |- (t = U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) -> ((A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t) <-> (A C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ A.r e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)A.s e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)(r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
26	20, 25	elab 2403	. . . . . . . 8 |- (U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) e. {t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} <-> (A C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ A.r e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)A.s e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)(r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
27		rdg0g 5152	. . . . . . . . . 10 |- (A e. B -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) = A)
28	27	adantr 425	. . . . . . . . 9 |- ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) = A)
29		peano1 3971	. . . . . . . . . . 11 |- (/) e. om
30		fveq2 4681	. . . . . . . . . . . 12 |- (x = (/) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)))
31	30	ssiun2s 3297	. . . . . . . . . . 11 |- ((/) e. om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
32	29, 31	ax-mp 7	. . . . . . . . . 10 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)
33	32	a1i 8	. . . . . . . . 9 |- ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
34	28, 33	eqsstr3d 2652	. . . . . . . 8 |- ((A e. B /\ A ~<_ om) -> A C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
35		ordtri2or2 3768	. . . . . . . . . . . . . . . . 17 |- ((Ord m /\ Ord n) -> (m C_ n \/ n C_ m))
36		nnord 3959	. . . . . . . . . . . . . . . . 17 |- (m e. om -> Ord m)
37		nnord 3959	. . . . . . . . . . . . . . . . 17 |- (n e. om -> Ord n)
38	35, 36, 37	syl2an 503	. . . . . . . . . . . . . . . 16 |- ((m e. om /\ n e. om) -> (m C_ n \/ n C_ m))
39	38	adantl 424	. . . . . . . . . . . . . . 15 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (m C_ n \/ n C_ m))
40		fictblem 15370	. . . . . . . . . . . . . . . . . . 19 |- (((A e. B /\ A ~<_ om) /\ (n e. om /\ m e. om)) -> (m C_ n -> ((s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) /\ r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)) -> E.x e. om (s i^i r) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
41		incom 2787	. . . . . . . . . . . . . . . . . . . . 21 |- (s i^i r) = (r i^i s)
42	41	eleq1i 1960	. . . . . . . . . . . . . . . . . . . 20 |- ((s i^i r) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
43	42	rexbii 2128	. . . . . . . . . . . . . . . . . . 19 |- (E.x e. om (s i^i r) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
44	40, 43	syl8ib 234	. . . . . . . . . . . . . . . . . 18 |- (((A e. B /\ A ~<_ om) /\ (n e. om /\ m e. om)) -> (m C_ n -> ((s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) /\ r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
45		ancom 482	. . . . . . . . . . . . . . . . . 18 |- ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) <-> (s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) /\ r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
46	44, 45	syl7ib 233	. . . . . . . . . . . . . . . . 17 |- (((A e. B /\ A ~<_ om) /\ (n e. om /\ m e. om)) -> (m C_ n -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
47	46	ancom2s 545	. . . . . . . . . . . . . . . 16 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (m C_ n -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
48		fictblem 15370	. . . . . . . . . . . . . . . 16 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (n C_ m -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
49	47, 48	jaod 469	. . . . . . . . . . . . . . 15 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> ((m C_ n \/ n C_ m) -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
50	39, 49	mpd 29	. . . . . . . . . . . . . 14 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
51	50	ex 402	. . . . . . . . . . . . 13 |- ((A e. B /\ A ~<_ om) -> ((m e. om /\ n e. om) -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
52	51	r19.23advv 2218	. . . . . . . . . . . 12 |- ((A e. B /\ A ~<_ om) -> (E.m e. om E.n e. om (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
53		reeanv 2249	. . . . . . . . . . . 12 |- (E.m e. om E.n e. om (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) <-> (E.m e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ E.n e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)))
54	52, 53	syl5ibr 224	. . . . . . . . . . 11 |- ((A e. B /\ A ~<_ om) -> ((E.m e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ E.n e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
55		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = m -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
56	55	eleq2d 1964	. . . . . . . . . . . . 13 |- (x = m -> (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
57	56	cbvrexv 2281	. . . . . . . . . . . 12 |- (E.x e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> E.m e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
58		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = n -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n))
59	58	eleq2d 1964	. . . . . . . . . . . . 13 |- (x = n -> (s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)))
60	59	cbvrexv 2281	. . . . . . . . . . . 12 |- (E.x e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> E.n e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n))
61	57, 60	anbi12i 540	. . . . . . . . . . 11 |- ((E.x e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ E.x e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)) <-> (E.m e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ E.n e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)))
62	54, 61	syl5ib 223	. . . . . . . . . 10 |- ((A e. B /\ A ~<_ om) -> ((E.x e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ E.x e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
63		eliun 3259	. . . . . . . . . . 11 |- (r e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> E.x e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
64		eliun 3259	. . . . . . . . . . 11 |- (s e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> E.x e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
65	63, 64	anbi12i 540	. . . . . . . . . 10 |- ((r e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ s e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)) <-> (E.x e. om r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ E.x e. om s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
66		eliun 3259	. . . . . . . . . 10 |- ((r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
67	62, 65, 66	3imtr4g 612	. . . . . . . . 9 |- ((A e. B /\ A ~<_ om) -> ((r e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ s e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)) -> (r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
68	67	r19.21aivv 2183	. . . . . . . 8 |- ((A e. B /\ A ~<_ om) -> A.r e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)A.s e. U_ x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)(r i^i s) e. U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
69	26, 34, 68	sylanbrc 527	. . . . . . 7 |- ((A e. B /\ A ~<_ om) -> U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) e. {t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)})
70		intss1 3231	. . . . . . 7 |- (U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) e. {t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} -> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
71	69, 70	syl 12	. . . . . 6 |- ((A e. B /\ A ~<_ om) -> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
72		ssdomg 5467	. . . . . 6 |- (|^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} e. _V -> (|^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} C_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) -> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} ~<_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x)))
73	17, 71, 72	sylc 83	. . . . 5 |- ((A e. B /\ A ~<_ om) -> |^|{t | (A C_ t /\ A.r e. t A.s e. t (r i^i s) e. t)} ~<_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
74	15, 73	eqbrtrd 3357	. . . 4 |- ((A e. B /\ A ~<_ om) -> ( fi ` A) ~<_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
75		domrefg 5452	. . . . . . 7 |- (om e. _V -> om ~<_ om)
76	18, 75	ax-mp 7	. . . . . 6 |- om ~<_ om
77	76	a1i 8	. . . . 5 |- ((A e. B /\ A ~<_ om) -> om ~<_ om)
78		fveq2 4681	. . . . . . . . . 10 |- (t = (/) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)))
79	78	breq1d 3348	. . . . . . . . 9 |- (t = (/) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) ~<_ om))
80	79	imbi2d 674	. . . . . . . 8 |- (t = (/) -> (((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om) <-> ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) ~<_ om)))
81		fveq2 4681	. . . . . . . . . 10 |- (t = k -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
82	81	breq1d 3348	. . . . . . . . 9 |- (t = k -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om))
83	82	imbi2d 674	. . . . . . . 8 |- (t = k -> (((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om) <-> ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)))
84		fveq2 4681	. . . . . . . . . 10 |- (t = suc k -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k))
85	84	breq1d 3348	. . . . . . . . 9 |- (t = suc k -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) ~<_ om))
86	85	imbi2d 674	. . . . . . . 8 |- (t = suc k -> (((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om) <-> ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) ~<_ om)))
87		fveq2 4681	. . . . . . . . . 10 |- (t = x -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
88	87	breq1d 3348	. . . . . . . . 9 |- (t = x -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om))
89	88	imbi2d 674	. . . . . . . 8 |- (t = x -> (((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` t) ~<_ om) <-> ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om)))
90		simpr 350	. . . . . . . . 9 |- ((A e. B /\ A ~<_ om) -> A ~<_ om)
91	28, 90	eqbrtrd 3357	. . . . . . . 8 |- ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` (/)) ~<_ om)
92		nnon 3957	. . . . . . . . . . . . . 14 |- (k e. om -> k e. On)
93		rdgsuc 5153	. . . . . . . . . . . . . 14 |- (k e. On -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
94	92, 93	syl 12	. . . . . . . . . . . . 13 |- (k e. om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
95	94	adantr 425	. . . . . . . . . . . 12 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
96		rexeq 2267	. . . . . . . . . . . . . . . . . . . 20 |- (u = r -> (E.z e. u w = (y i^i z) <-> E.z e. r w = (y i^i z)))
97	96	rexeqbi1dv 2272	. . . . . . . . . . . . . . . . . . 19 |- (u = r -> (E.y e. u E.z e. u w = (y i^i z) <-> E.y e. r E.z e. r w = (y i^i z)))
98	97	abbidv 2008	. . . . . . . . . . . . . . . . . 18 |- (u = r -> {w | E.y e. u E.z e. u w = (y i^i z)} = {w | E.y e. r E.z e. r w = (y i^i z)})
99	98	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (u = r -> (v = {w | E.y e. u E.z e. u w = (y i^i z)} <-> v = {w | E.y e. r E.z e. r w = (y i^i z)}))
100		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (v = s -> (v = {w | E.y e. r E.z e. r w = (y i^i z)} <-> s = {w | E.y e. r E.z e. r w = (y i^i z)}))
101	99, 100	sylan9bb 599	. . . . . . . . . . . . . . . 16 |- ((u = r /\ v = s) -> (v = {w | E.y e. u E.z e. u w = (y i^i z)} <-> s = {w | E.y e. r E.z e. r w = (y i^i z)}))
102	101	cbvopabv 3404	. . . . . . . . . . . . . . 15 |- {<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}} = {<.r, s>. | s = {w | E.y e. r E.z e. r w = (y i^i z)}}
103		eqeq1 1890	. . . . . . . . . . . . . . . . . . . 20 |- (w = c -> (w = (y i^i z) <-> c = (y i^i z)))
104	103	2rexbidv 2141	. . . . . . . . . . . . . . . . . . 19 |- (w = c -> (E.y e. r E.z e. r w = (y i^i z) <-> E.y e. r E.z e. r c = (y i^i z)))
105	104	cbvabv 2420	. . . . . . . . . . . . . . . . . 18 |- {w | E.y e. r E.z e. r w = (y i^i z)} = {c | E.y e. r E.z e. r c = (y i^i z)}
106		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = m -> (y i^i z) = (m i^i z))
107	106	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = m -> (c = (y i^i z) <-> c = (m i^i z)))
108	107	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . 21 |- (y = m -> (E.z e. r c = (y i^i z) <-> E.z e. r c = (m i^i z)))
109	108	cbvrexv 2281	. . . . . . . . . . . . . . . . . . . 20 |- (E.y e. r E.z e. r c = (y i^i z) <-> E.m e. r E.z e. r c = (m i^i z))
110		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = n -> (m i^i z) = (m i^i n))
111	110	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = n -> (c = (m i^i z) <-> c = (m i^i n)))
112	111	cbvrexv 2281	. . . . . . . . . . . . . . . . . . . . 21 |- (E.z e. r c = (m i^i z) <-> E.n e. r c = (m i^i n))
113	112	rexbii 2128	. . . . . . . . . . . . . . . . . . . 20 |- (E.m e. r E.z e. r c = (m i^i z) <-> E.m e. r E.n e. r c = (m i^i n))
114	109, 113	bitri 190	. . . . . . . . . . . . . . . . . . 19 |- (E.y e. r E.z e. r c = (y i^i z) <-> E.m e. r E.n e. r c = (m i^i n))
115	114	abbii 2006	. . . . . . . . . . . . . . . . . 18 |- {c | E.y e. r E.z e. r c = (y i^i z)} = {c | E.m e. r E.n e. r c = (m i^i n)}
116	105, 115	eqtri 1908	. . . . . . . . . . . . . . . . 17 |- {w | E.y e. r E.z e. r w = (y i^i z)} = {c | E.m e. r E.n e. r c = (m i^i n)}
117	116	eqeq2i 1894	. . . . . . . . . . . . . . . 16 |- (s = {w | E.y e. r E.z e. r w = (y i^i z)} <-> s = {c | E.m e. r E.n e. r c = (m i^i n)})
118	117	opabbii 3402	. . . . . . . . . . . . . . 15 |- {<.r, s>. | s = {w | E.y e. r E.z e. r w = (y i^i z)}} = {<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}
119	102, 118	eqtri 1908	. . . . . . . . . . . . . 14 |- {<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}} = {<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}
120	119	fveq1i 4682	. . . . . . . . . . . . 13 |- ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) = ({<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
121		fvex 4689	. . . . . . . . . . . . . 14 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) e. _V
122	121	abrexex 4836	. . . . . . . . . . . . . . 15 |- {c | E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} e. _V
123	121, 122	abrexex2 4847	. . . . . . . . . . . . . 14 |- {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} e. _V
124		rexeq 2267	. . . . . . . . . . . . . . . 16 |- (r = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> (E.n e. r c = (m i^i n) <-> E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
125	124	rexeqbi1dv 2272	. . . . . . . . . . . . . . 15 |- (r = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> (E.m e. r E.n e. r c = (m i^i n) <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
126	125	abbidv 2008	. . . . . . . . . . . . . 14 |- (r = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> {c | E.m e. r E.n e. r c = (m i^i n)} = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
127	121, 123, 126	fvopab 4753	. . . . . . . . . . . . 13 |- ({<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}
128	120, 127	eqtri 1908	. . . . . . . . . . . 12 |- ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}
129	95, 128	syl6eq 1944	. . . . . . . . . . 11 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
130		simplr 449	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
131		simpr 350	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
132		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- m e. _V
133	132	inex1 3452	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m i^i n) e. _V
134	133	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> (m i^i n) e. _V)
135		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a = m -> (a i^i b) = (m i^i b))
136		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b = n -> (m i^i b) = (m i^i n))
137		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . 23 |- {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} = {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}
138	135, 136, 137	oprabval2g 4956	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ (m i^i n) e. _V) -> (m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = (m i^i n))
139	130, 131, 134, 138	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 |- ((((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> (m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = (m i^i n))
140	139	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . 20 |- ((((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> ((m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = c <-> (m i^i n) = c))
141		eqcom 1886	. . . . . . . . . . . . . . . . . . . 20 |- ((m i^i n) = c <-> c = (m i^i n))
142	140, 141	syl6bb 595	. . . . . . . . . . . . . . . . . . 19 |- ((((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> ((m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = c <-> c = (m i^i n)))
143	142	rexbidva 2120	. . . . . . . . . . . . . . . . . 18 |- (((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) /\ m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> (E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)(m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = c <-> E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
144	143	rexbidva 2120	. . . . . . . . . . . . . . . . 17 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> (E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)(m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = c <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
145		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- a e. _V
146	145	inex1 3452	. . . . . . . . . . . . . . . . . . 19 |- (a i^i b) e. _V
147	146, 137	fnoprab2 5064	. . . . . . . . . . . . . . . . . 18 |- {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} Fn ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
148		oprvelrn 4969	. . . . . . . . . . . . . . . . . 18 |- ({<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} Fn ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) -> (c e. ran {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)(m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = c))
149	147, 148	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (c e. ran {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)(m{<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}n) = c)
150	144, 149	syl5bb 591	. . . . . . . . . . . . . . . 16 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> (c e. ran {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
151	150	abbi2dv 2009	. . . . . . . . . . . . . . 15 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> ran {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
152	151, 147	jctil 316	. . . . . . . . . . . . . 14 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> ({<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} Fn ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ ran {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}))
153		df-fo 4012	. . . . . . . . . . . . . 14 |- ({<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}:((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))-onto->{c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} <-> ({<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} Fn ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ ran {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))} = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}))
154	152, 153	sylibr 217	. . . . . . . . . . . . 13 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> {<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}:((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))-onto->{c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
155	121, 121	xpex 4096	. . . . . . . . . . . . . 14 |- ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) e. _V
156	155	fodom 5960	. . . . . . . . . . . . 13 |- ({<.<.a, b>., t>. | ((a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ t = (a i^i b))}:((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))-onto->{c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} -> {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} ~<_ ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
157	154, 156	syl 12	. . . . . . . . . . . 12 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} ~<_ ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
158	18, 121	xpdom1 5502	. . . . . . . . . . . . . . 15 |- ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
159	18, 18	xpdom2 5501	. . . . . . . . . . . . . . 15 |- ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om -> (om X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. om))
160		domtr 5474	. . . . . . . . . . . . . . 15 |- ((((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ (om X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. om)) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. om))
161	158, 159, 160	syl11anc 524	. . . . . . . . . . . . . 14 |- ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. om))
162	161	ad2antll 443	. . . . . . . . . . . . 13 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. om))
163		xpomen 8769	. . . . . . . . . . . . . 14 |- (om X. om) ~~ om
164	163	a1i 8	. . . . . . . . . . . . 13 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> (om X. om) ~~ om)
165		domentr 5480	. . . . . . . . . . . . 13 |- ((((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ (om X. om) /\ (om X. om) ~~ om) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ om)
166	162, 164, 165	syl11anc 524	. . . . . . . . . . . 12 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ om)
167		domtr 5474	. . . . . . . . . . . 12 |- (({c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} ~<_ ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) /\ ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) X. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) ~<_ om) -> {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} ~<_ om)
168	157, 166, 167	syl11anc 524	. . . . . . . . . . 11 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} ~<_ om)
169	129, 168	eqbrtrd 3357	. . . . . . . . . 10 |- ((k e. om /\ ((A e. B /\ A ~<_ om) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om)) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) ~<_ om)
170	169	exp32 408	. . . . . . . . 9 |- (k e. om -> ((A e. B /\ A ~<_ om) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) ~<_ om)))
171	170	a2d 16	. . . . . . . 8 |- (k e. om -> (((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) ~<_ om) -> ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) ~<_ om)))
172	80, 83, 86, 89, 91, 171	finds 3979	. . . . . . 7 |- (x e. om -> ((A e. B /\ A ~<_ om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om))
173	172	com12 14	. . . . . 6 |- ((A e. B /\ A ~<_ om) -> (x e. om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om))
174	173	r19.21aiv 2175	. . . . 5 |- ((A e. B /\ A ~<_ om) -> A.x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om)
175	18, 19	iunctb 8844	. . . . 5 |- ((om ~<_ om /\ A.x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om) -> U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om)
176	77, 174, 175	syl11anc 524	. . . 4 |- ((A e. B /\ A ~<_ om) -> U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om)
177		domtr 5474	. . . 4 |- ((( fi ` A) ~<_ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) /\ U_x e. om (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) ~<_ om) -> ( fi ` A) ~<_ om)
178	74, 176, 177	syl11anc 524	. . 3 |- ((A e. B /\ A ~<_ om) -> ( fi ` A) ~<_ om)
179	178	ex 402	. 2 |- (A e. B -> (A ~<_ om -> ( fi ` A) ~<_ om))
180		abfi2 10216	. . . 4 |- (A e. B -> A C_ ( fi ` A))
181		ssdomg 5467	. . . 4 |- (A e. B -> (A C_ ( fi ` A) -> A ~<_ ( fi ` A)))
182	180, 181	mpd 29	. . 3 |- (A e. B -> A ~<_ ( fi ` A))
183		domtr 5474	. . . 4 |- ((A ~<_ ( fi ` A) /\ ( fi ` A) ~<_ om) -> A ~<_ om)
184	183	ex 402	. . 3 |- (A ~<_ ( fi ` A) -> (( fi ` A) ~<_ om -> A ~<_ om))
185	182, 184	syl 12	. 2 |- (A e. B -> (( fi ` A) ~<_ om -> A ~<_ om))
186	179, 185	impbid 574	1 |- (A e. B -> (A ~<_ om <-> ( fi ` A) ~<_ om))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  |^|cint 3214  U_ciun 3255   class class class wbr 3338  {copab 3395  Ord word 3656  Oncon0 3657  suc csuc 3659  omcom 3949   X. cxp 3984  ran crn 3987   Fn wfn 3993  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884  {copab2 4885  reccrdg 5139   ~~ cen 5423   ~<_ cdom 5424  Fincfn 5426   fi cfi 10210

This theorem is referenced by:  2ndcsb 15476

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-2o 5178  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-undef 5556  df-riota 5560  df-r1 5750  df-rank 5751  df-card 5862  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-seq1 7721  df-exp 7812  df-fi 10211

Copyright terms: Public domain