Theorem funcnvuni 4482

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

Assertion

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

Distinct variable group:   f,g,A

Proof of Theorem funcnvuni

Step	Hyp	Ref	Expression
1		cnveq 4135	. . . . . . . . . . 11 |- (f = v -> `'f = `'v)
2		funeq 4441	. . . . . . . . . . 11 |- (`'f = `'v -> (Fun `'f <-> Fun `'v))
3	1, 2	syl 12	. . . . . . . . . 10 |- (f = v -> (Fun `'f <-> Fun `'v))
4		sseq1 2637	. . . . . . . . . . . 12 |- (f = v -> (f C_ g <-> v C_ g))
5		sseq2 2639	. . . . . . . . . . . 12 |- (f = v -> (g C_ f <-> g C_ v))
6	4, 5	orbi12d 689	. . . . . . . . . . 11 |- (f = v -> ((f C_ g \/ g C_ f) <-> (v C_ g \/ g C_ v)))
7	6	ralbidv 2123	. . . . . . . . . 10 |- (f = v -> (A.g e. A (f C_ g \/ g C_ f) <-> A.g e. A (v C_ g \/ g C_ v)))
8	3, 7	anbi12d 690	. . . . . . . . 9 |- (f = v -> ((Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) <-> (Fun `'v /\ A.g e. A (v C_ g \/ g C_ v))))
9	8	rcla4v 2376	. . . . . . . 8 |- (v e. A -> (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> (Fun `'v /\ A.g e. A (v C_ g \/ g C_ v))))
10		funeq 4441	. . . . . . . . . 10 |- (z = `'v -> (Fun z <-> Fun `'v))
11	10	biimprcd 173	. . . . . . . . 9 |- (Fun `'v -> (z = `'v -> Fun z))
12		sseq2 2639	. . . . . . . . . . . . . . 15 |- (g = x -> (v C_ g <-> v C_ x))
13		sseq1 2637	. . . . . . . . . . . . . . 15 |- (g = x -> (g C_ v <-> x C_ v))
14	12, 13	orbi12d 689	. . . . . . . . . . . . . 14 |- (g = x -> ((v C_ g \/ g C_ v) <-> (v C_ x \/ x C_ v)))
15	14	rcla4v 2376	. . . . . . . . . . . . 13 |- (x e. A -> (A.g e. A (v C_ g \/ g C_ v) -> (v C_ x \/ x C_ v)))
16		sseq12 2640	. . . . . . . . . . . . . . . . 17 |- ((z = `'v /\ w = `'x) -> (z C_ w <-> `'v C_ `'x))
17	16	ancoms 484	. . . . . . . . . . . . . . . 16 |- ((w = `'x /\ z = `'v) -> (z C_ w <-> `'v C_ `'x))
18		sseq12 2640	. . . . . . . . . . . . . . . 16 |- ((w = `'x /\ z = `'v) -> (w C_ z <-> `'x C_ `'v))
19	17, 18	orbi12d 689	. . . . . . . . . . . . . . 15 |- ((w = `'x /\ z = `'v) -> ((z C_ w \/ w C_ z) <-> (`'v C_ `'x \/ `'x C_ `'v)))
20		cnvss 4134	. . . . . . . . . . . . . . . 16 |- (v C_ x -> `'v C_ `'x)
21		cnvss 4134	. . . . . . . . . . . . . . . 16 |- (x C_ v -> `'x C_ `'v)
22	20, 21	orim12i 363	. . . . . . . . . . . . . . 15 |- ((v C_ x \/ x C_ v) -> (`'v C_ `'x \/ `'x C_ `'v))
23	19, 22	syl5cbir 228	. . . . . . . . . . . . . 14 |- ((v C_ x \/ x C_ v) -> ((w = `'x /\ z = `'v) -> (z C_ w \/ w C_ z)))
24	23	exp3a 405	. . . . . . . . . . . . 13 |- ((v C_ x \/ x C_ v) -> (w = `'x -> (z = `'v -> (z C_ w \/ w C_ z))))
25	15, 24	syl6com 64	. . . . . . . . . . . 12 |- (A.g e. A (v C_ g \/ g C_ v) -> (x e. A -> (w = `'x -> (z = `'v -> (z C_ w \/ w C_ z)))))
26	25	r19.23adv 2215	. . . . . . . . . . 11 |- (A.g e. A (v C_ g \/ g C_ v) -> (E.x e. A w = `'x -> (z = `'v -> (z C_ w \/ w C_ z))))
27	26	com23 36	. . . . . . . . . 10 |- (A.g e. A (v C_ g \/ g C_ v) -> (z = `'v -> (E.x e. A w = `'x -> (z C_ w \/ w C_ z))))
28	27	19.21adv 1666	. . . . . . . . 9 |- (A.g e. A (v C_ g \/ g C_ v) -> (z = `'v -> A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z))))
29	11, 28	anim12ii 618	. . . . . . . 8 |- ((Fun `'v /\ A.g e. A (v C_ g \/ g C_ v)) -> (z = `'v -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))))
30	9, 29	syl6com 64	. . . . . . 7 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> (v e. A -> (z = `'v -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z))))))
31	30	r19.23adv 2215	. . . . . 6 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> (E.v e. A z = `'v -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))))
32		cnveq 4135	. . . . . . . 8 |- (x = v -> `'x = `'v)
33	32	eqeq2d 1895	. . . . . . 7 |- (x = v -> (z = `'x <-> z = `'v))
34	33	cbvrexv 2281	. . . . . 6 |- (E.x e. A z = `'x <-> E.v e. A z = `'v)
35	31, 34	syl5ib 223	. . . . 5 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> (E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))))
36	35	19.21aiv 1664	. . . 4 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.z(E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))))
37		df-ral 2109	. . . . 5 |- (A.z e. {y | E.x e. A y = `'x} (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ 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 C_ w \/ w C_ z))))
38		visset 2295	. . . . . . . 8 |- z e. _V
39		eqeq1 1890	. . . . . . . . 9 |- (y = z -> (y = `'x <-> z = `'x))
40	39	rexbidv 2124	. . . . . . . 8 |- (y = z -> (E.x e. A y = `'x <-> E.x e. A z = `'x))
41	38, 40	elab 2403	. . . . . . 7 |- (z e. {y | E.x e. A y = `'x} <-> E.x e. A z = `'x)
42		eqeq1 1890	. . . . . . . . . 10 |- (y = w -> (y = `'x <-> w = `'x))
43	42	rexbidv 2124	. . . . . . . . 9 |- (y = w -> (E.x e. A y = `'x <-> E.x e. A w = `'x))
44	43	ralab 2417	. . . . . . . 8 |- (A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ z) <-> A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))
45	44	anbi2i 538	. . . . . . 7 |- ((Fun z /\ A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ z)) <-> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z))))
46	41, 45	imbi12i 205	. . . . . 6 |- ((z e. {y | E.x e. A y = `'x} -> (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ z))) <-> (E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))))
47	46	albii 1346	. . . . 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 C_ w \/ w C_ z))) <-> A.z(E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))))
48	37, 47	bitr2i 191	. . . 4 |- (A.z(E.x e. A z = `'x -> (Fun z /\ A.w(E.x e. A w = `'x -> (z C_ w \/ w C_ z)))) <-> A.z e. {y | E.x e. A y = `'x} (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ z)))
49	36, 48	sylib 215	. . 3 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.z e. {y | E.x e. A y = `'x} (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ z)))
50		fununi 4481	. . 3 |- (A.z e. {y | E.x e. A y = `'x} (Fun z /\ A.w e. {y | E.x e. A y = `'x} (z C_ w \/ w C_ z)) -> Fun U.{y | E.x e. A y = `'x})
51	49, 50	syl 12	. 2 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> Fun U.{y | E.x e. A y = `'x})
52		cnvuni 4147	. . . 4 |- `'U.A = U_x e. A `'x
53		visset 2295	. . . . . 6 |- x e. _V
54	53	cnvex 4425	. . . . 5 |- `'x e. _V
55	54	dfiun2 3285	. . . 4 |- U_x e. A `'x = U.{y | E.x e. A y = `'x}
56	52, 55	eqtri 1908	. . 3 |- `'U.A = U.{y | E.x e. A y = `'x}
57		funeq 4441	. . 3 |- (`'U.A = U.{y | E.x e. A y = `'x} -> (Fun `'U.A <-> Fun U.{y | E.x e. A y = `'x}))
58	56, 57	ax-mp 7	. 2 |- (Fun `'U.A <-> Fun U.{y | E.x e. A y = `'x})
59	51, 58	sylibr 217	1 |- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> Fun `'U.A)

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  E.wrex 2106   C_ wss 2593  U.cuni 3177  U_ciun 3255  `'ccnv 3985  Fun wfun 3992

This theorem is referenced by:  fun11uni 4483

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-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-fun 4008

Copyright terms: Public domain