funcnvuni - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem funcnvuni 3570

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

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

Distinct variable group:

**Proof of Theorem funcnvuni**
Step	Hyp	Ref	Expression
1		cnveq 3298	. . . . . . . . . . 11
2		funeq 3541	. . . . . . . . . . 11
3	1, 2	syl 10	. . . . . . . . . 10
4		sseq1 2085	. . . . . . . . . . . 12
5		sseq2 2086	. . . . . . . . . . . 12
6	4, 5	orbi12d 629	. . . . . . . . . . 11 $\/$ $\/$
7	6	ralbidv 1666	. . . . . . . . . 10 $\/$ $\/$
8	3, 7	anbi12d 630	. . . . . . . . 9 $/\$ $\/$ $/\$ $\/$
9	8	rcla4v 1876	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
10		funeq 3541	. . . . . . . . . 10
11	10	biimprcd 156	. . . . . . . . 9
12		sseq2 2086	. . . . . . . . . . . . . . 15
13		sseq1 2085	. . . . . . . . . . . . . . 15
14	12, 13	orbi12d 629	. . . . . . . . . . . . . 14 $\/$ $\/$
15	14	rcla4v 1876	. . . . . . . . . . . . 13 $\/$ $\/$
16		sseq12 2087	. . . . . . . . . . . . . . . . 17 $/\$
17	16	ancoms 438	. . . . . . . . . . . . . . . 16 $/\$
18		sseq12 2087	. . . . . . . . . . . . . . . 16 $/\$
19	17, 18	orbi12d 629	. . . . . . . . . . . . . . 15 $/\$ $\/$ $\/$
20		cnvss 3297	. . . . . . . . . . . . . . . 16
21		cnvss 3297	. . . . . . . . . . . . . . . 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 1749	. . . . . . . . . . 11 $\/$ $\/$
27	26	com23 32	. . . . . . . . . 10 $\/$ $\/$
28	27	19.21adv 1290	. . . . . . . . 9 $\/$ $\/$
29	11, 28	anim12ii 561	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
30	9, 29	syl6com 53	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
31	30	r19.23adv 1749	. . . . . 6 $/\$ $\/$ $/\$ $\/$
32		cnveq 3298	. . . . . . . 8
33	32	eqeq2d 1489	. . . . . . 7
34	33	cbvrexv 1804	. . . . . 6
35	31, 34	syl5ib 206	. . . . 5 $/\$ $\/$ $/\$ $\/$
36	35	19.21aiv 1288	. . . 4 $/\$ $\/$ $/\$ $\/$
37		df-ral 1652	. . . . 5 $/\$ $\/$ $/\$ $\/$
38		visset 1816	. . . . . . . 8
39		eqeq1 1484	. . . . . . . . 9
40	39	rexbidv 1667	. . . . . . . 8
41	38, 40	elab 1900	. . . . . . 7
42		df-ral 1652	. . . . . . . . 9 $\/$ $\/$
43		visset 1816	. . . . . . . . . . . 12
44		eqeq1 1484	. . . . . . . . . . . . 13
45	44	rexbidv 1667	. . . . . . . . . . . 12
46	43, 45	elab 1900	. . . . . . . . . . 11
47	46	imbi1i 186	. . . . . . . . . 10 $\/$ $\/$
48	47	albii 1001	. . . . . . . . 9 $\/$ $\/$
49	42, 48	bitr 173	. . . . . . . 8 $\/$ $\/$
50	49	anbi2i 482	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
51	41, 50	imbi12i 188	. . . . . 6 $/\$ $\/$ $/\$ $\/$
52	51	albii 1001	. . . . 5 $/\$ $\/$ $/\$ $\/$
53	37, 52	bitr2 174	. . . 4 $/\$ $\/$ $/\$ $\/$
54	36, 53	sylib 198	. . 3 $/\$ $\/$