funcnvuni - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem funcnvuni 3580

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

**Assertion**
Ref	Expression
funcnvuni	$/\$ $\/$

Distinct variable group:

**Proof of Theorem funcnvuni**
Step	Hyp	Ref	Expression
1		cnveq 3308	. . . . . . . . . . 11
2		funeq 3551	. . . . . . . . . . 11
3	1, 2	syl 10	. . . . . . . . . 10
4		sseq1 2093	. . . . . . . . . . . 12
5		sseq2 2094	. . . . . . . . . . . 12
6	4, 5	orbi12d 630	. . . . . . . . . . 11 $\/$ $\/$
7	6	ralbidv 1670	. . . . . . . . . 10 $\/$ $\/$
8	3, 7	anbi12d 631	. . . . . . . . 9 $/\$ $\/$ $/\$ $\/$
9	8	rcla4v 1880	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
10		funeq 3551	. . . . . . . . . 10
11	10	biimprcd 156	. . . . . . . . 9
12		sseq2 2094	. . . . . . . . . . . . . . 15
13		sseq1 2093	. . . . . . . . . . . . . . 15
14	12, 13	orbi12d 630	. . . . . . . . . . . . . 14 $\/$ $\/$
15	14	rcla4v 1880	. . . . . . . . . . . . 13 $\/$ $\/$
16		sseq12 2095	. . . . . . . . . . . . . . . . 17 $/\$
17	16	ancoms 439	. . . . . . . . . . . . . . . 16 $/\$
18		sseq12 2095	. . . . . . . . . . . . . . . 16 $/\$
19	17, 18	orbi12d 630	. . . . . . . . . . . . . . 15 $/\$ $\/$ $\/$
20		cnvss 3307	. . . . . . . . . . . . . . . 16
21		cnvss 3307	. . . . . . . . . . . . . . . 16
22	20, 21	orim12i 336	. . . . . . . . . . . . . . 15 $\/$ $\/$
23	19, 22	syl5cbir 211	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$
24	23	exp3a 376	. . . . . . . . . . . . 13 $\/$ $\/$
25	15, 24	syl6com 53	. . . . . . . . . . . 12 $\/$ $\/$
26	25	r19.23adv 1753	. . . . . . . . . . 11 $\/$ $\/$
27	26	com23 32	. . . . . . . . . 10 $\/$ $\/$
28	27	19.21adv 1292	. . . . . . . . 9 $\/$ $\/$
29	11, 28	anim12ii 562	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
30	9, 29	syl6com 53	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
31	30	r19.23adv 1753	. . . . . 6 $/\$ $\/$ $/\$ $\/$
32		cnveq 3308	. . . . . . . 8
33	32	eqeq2d 1493	. . . . . . 7
34	33	cbvrexv 1808	. . . . . 6
35	31, 34	syl5ib 206	. . . . 5 $/\$ $\/$ $/\$ $\/$
36	35	19.21aiv 1290	. . . 4 $/\$ $\/$ $/\$ $\/$
37		df-ral 1656	. . . . 5 $/\$ $\/$ $/\$ $\/$
38		visset 1820	. . . . . . . 8
39		eqeq1 1488	. . . . . . . . 9
40	39	rexbidv 1671	. . . . . . . 8
41	38, 40	elab 1904	. . . . . . 7
42		df-ral 1656	. . . . . . . . 9 $\/$ $\/$
43		visset 1820	. . . . . . . . . . . 12
44		eqeq1 1488	. . . . . . . . . . . . 13
45	44	rexbidv 1671	. . . . . . . . . . . 12
46	43, 45	elab 1904	. . . . . . . . . . 11
47	46	imbi1i 186	. . . . . . . . . 10 $\/$ $\/$
48	47	albii 1003	. . . . . . . . 9 $\/$ $\/$
49	42, 48	bitri 173	. . . . . . . 8 $\/$ $\/$
50	49	anbi2i 483	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
51	41, 50	imbi12i 188	. . . . . 6 $/\$ $\/$ $/\$ $\/$
52	51	albii 1003	. . . . 5 $/\$ $\/$ $/\$ $\/$
53	37, 52	bitr2i 174	. . . 4 $/\$ $\/$ $/\$ $\/$
54	36, 53	sylib 198	. . 3 $/\$ $\/$