Theorem funcnvuni 2706

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 2703 for "single-rooted" definition.)

Assertion

Ref	Expression
funcnvuni	|- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> Fun `'U.A)

Distinct variable group(s):   f,g,A

Proof of Theorem funcnvuni

Step	Hyp	Ref	Expression
1		cnveq 2513	. . . . . . . . . . 11 |- (f = v -> `'f = `'v)
2		funeq 2683	. . . . . . . . . . 11 |- (`'f = `'v -> (Fun `'f <-> Fun `'v))
3	1, 2	syl 12	. . . . . . . . . 10 |- (f = v -> (Fun `'f <-> Fun `'v))
4		sseq1 1521	. . . . . . . . . . . 12 |- (f = v -> (f (_ g <-> v (_ g))
5		sseq2 1522	. . . . . . . . . . . 12 |- (f = v -> (g (_ f <-> g (_ v))
6	4, 5	orbi12d 475	. . . . . . . . . . 11 |- (f = v -> ((f (_ g \/ g (_ f) <-> (v (_ g \/ g (_ v)))
7	6	biraldv 1219	. . . . . . . . . 10 |- (f = v -> (A.g e. A (f (_ g \/ g (_ f) <-> A.g e. A (v (_ g \/ g (_ v)))
8	3, 7	anbi12d 476	. . . . . . . . 9 |- (f = v -> ((Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) <-> (Fun `'v /\ A.g e. A (v (_ g \/ g (_ v))))
9	8	rcla4v 1402	. . . . . . . 8 |- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> (v e. A -> (Fun `'v /\ A.g e. A (v (_ g \/ g (_ v))))
10		funeq 2683	. . . . . . . . . . 11 |- (z = `'v -> (Fun z <-> Fun `'v))
11	10	biimprcd 138	. . . . . . . . . 10 |- (Fun `'v -> (z = `'v -> Fun z))
12	11	adantr 306	. . . . . . . . 9 |- ((Fun `'v /\ A.g e. A (v (_ g \/ g (_ v)) -> (z = `'v -> Fun z))
13		sseq2 1522	. . . . . . . . . . . . . . . 16 |- (g = x -> (v (_ g <-> v (_ x))
14		sseq1 1521	. . . . . . . . . . . . . . . 16 |- (g = x -> (g (_ v <-> x (_ v))
15	13, 14	orbi12d 475	. . . . . . . . . . . . . . 15 |- (g = x -> ((v (_ g \/ g (_ v) <-> (v (_ x \/ x (_ v)))
16	15	rcla4v 1402	. . . . . . . . . . . . . 14 |- (A.g e. A (v (_ g \/ g (_ v) -> (x e. A -> (v (_ x \/ x (_ v)))
17		sseq12 1523	. . . . . . . . . . . . . . . . . . 19 |- ((z = `'v /\ w = `'x) -> (z (_ w <-> `'v (_ `'x))
18	17	ancoms 334	. . . . . . . . . . . . . . . . . 18 |- ((w = `'x /\ z = `'v) -> (z (_ w <-> `'v (_ `'x))
19		sseq12 1523	. . . . . . . . . . . . . . . . . 18 |- ((w = `'x /\ z = `'v) -> (w (_ z <-> `'x (_ `'v))
20	18, 19	orbi12d 475	. . . . . . . . . . . . . . . . 17 |- ((w = `'x /\ z = `'v) -> ((z (_ w \/ w (_ z) <-> (`'v (_ `'x \/ `'x (_ `'v)))
21		cnvss 2512	. . . . . . . . . . . . . . . . . 18 |- (v (_ x -> `'v (_ `'x)
22		cnvss 2512	. . . . . . . . . . . . . . . . . 18 |- (x (_ v -> `'x (_ `'v)
23	21, 22	orim12i 271	. . . . . . . . . . . . . . . . 17 |- ((v (_ x \/ x (_ v) -> (`'v (_ `'x \/ `'x (_ `'v))
24	20, 23	syl5bir 184	. . . . . . . . . . . . . . . 16 |- ((w = `'x /\ z = `'v) -> ((v (_ x \/ x (_ v) -> (z (_ w \/ w (_ z)))
25	24	com12 13	. . . . . . . . . . . . . . 15 |- ((v (_ x \/ x (_ v) -> ((w = `'x /\ z = `'v) -> (z (_ w \/ w (_ z)))
26	25	exp3a 292	. . . . . . . . . . . . . 14 |- ((v (_ x \/ x (_ v) -> (w = `'x -> (z = `'v -> (z (_ w \/ w (_ z))))
27	16, 26	syl6 23	. . . . . . . . . . . . 13 |- (A.g e. A (v (_ g \/ g (_ v) -> (x e. A -> (w = `'x -> (z = `'v -> (z (_ w \/ w (_ z)))))
28	27	r19.23adv 1286	. . . . . . . . . . . 12 |- (A.g e. A (v (_ g \/ g (_ v) -> (E.x e. A w = `'x -> (z = `'v -> (z (_ w \/ w (_ z))))
29	28	com23 32	. . . . . . . . . . 11 |- (A.g e. A (v (_ g \/ g (_ v) -> (z = `'v -> (E.x e. A w = `'x -> (z (_ w \/ w (_ z))))
30	29	19.21adv 945	. . . . . . . . . 10 |- (A.g e. A (v (_ g \/ g (_ v) -> (z = `'v -> A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z))))
31	30	adantl 305	. . . . . . . . 9 |- ((Fun `'v /\ A.g e. A (v (_ g \/ g (_ v)) -> (z = `'v -> A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z))))
32	12, 31	jcad 455	. . . . . . . 8 |- ((Fun `'v /\ A.g e. A (v (_ g \/ g (_ v)) -> (z = `'v -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))))
33	9, 32	syl6 23	. . . . . . 7 |- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> (v e. A -> (z = `'v -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z))))))
34	33	r19.23adv 1286	. . . . . 6 |- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> (E.v e. A z = `'v -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))))
35		cnveq 2513	. . . . . . . 8 |- (x = v -> `'x = `'v)
36	35	cleq2d 1112	. . . . . . 7 |- (x = v -> (z = `'x <-> z = `'v))
37	36	cbvrexv 1334	. . . . . 6 |- (E.x e. A z = `'x <-> E.v e. A z = `'v)
38	34, 37	syl5ib 181	. . . . 5 |- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> (E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))))
39	38	19.21aiv 943	. . . 4 |- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> A.z(E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))))
40		df-ral 1205	. . . . 5 |- (A.z e. {y | E.x e. A y = `'x} (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z)) <-> A.z(z e. {y | E.x e. A y = `'x} -> (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z))))
41		visset 1350	. . . . . . . 8 |- z e. V
42		cleq1 1107	. . . . . . . . 9 |- (y = z -> (y = `'x <-> z = `'x))
43	42	birexdv 1220	. . . . . . . 8 |- (y = z -> (E.x e. A y = `'x <-> E.x e. A z = `'x))
44	41, 43	elab 1415	. . . . . . 7 |- (z e. {y | E.x e. A y = `'x} <-> E.x e. A z = `'x)
45		df-ral 1205	. . . . . . . . 9 |- (A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z) <-> A.w(w e. {y | E.x e. A y = `'x} -> (z (_ w \/ w (_ z)))
46		visset 1350	. . . . . . . . . . . 12 |- w e. V
47		cleq1 1107	. . . . . . . . . . . . 13 |- (y = w -> (y = `'x <-> w = `'x))
48	47	birexdv 1220	. . . . . . . . . . . 12 |- (y = w -> (E.x e. A y = `'x <-> E.x e. A w = `'x))
49	46, 48	elab 1415	. . . . . . . . . . 11 |- (w e. {y | E.x e. A y = `'x} <-> E.x e. A w = `'x)
50	49	imbi1i 161	. . . . . . . . . 10 |- ((w e. {y | E.x e. A y = `'x} -> (z (_ w \/ w (_ z)) <-> (E.x e. A w = `'x -> (z (_ w \/ w (_ z)))
51	50	bial 695	. . . . . . . . 9 |- (A.w(w e. {y | E.x e. A y = `'x} -> (z (_ w \/ w (_ z)) <-> A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))
52	45, 51	bitr 151	. . . . . . . 8 |- (A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z) <-> A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))
53	52	anbi2i 367	. . . . . . 7 |- ((Fun z /\ A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z)) <-> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z))))
54	44, 53	imbi12i 163	. . . . . 6 |- ((z e. {y | E.x e. A y = `'x} -> (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z))) <-> (E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))))
55	54	bial 695	. . . . 5 |- (A.z(z e. {y | E.x e. A y = `'x} -> (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z (_ w \/ w (_ z))) <-> A.z(E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))))
56	40, 55	bitr2 152	. . . 4 |- (A.z(E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z (_ w \/ w (_ z)))) <-> A.z e. {y | E.x e. A y = `'x}