Theorem funcnvuni

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004)

	Ref	Expression
Assertion	funcnvuni	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ◡ ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cnveq	⊢ ( 𝑥 = 𝑣 → ◡ 𝑥 = ◡ 𝑣 )
2	1	eqeq2d	⊢ ( 𝑥 = 𝑣 → ( 𝑧 = ◡ 𝑥 ↔ 𝑧 = ◡ 𝑣 ) )
3	2	cbvrexvw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 ↔ ∃ 𝑣 ∈ 𝐴 𝑧 = ◡ 𝑣 )
4		cnveq	⊢ ( 𝑓 = 𝑣 → ◡ 𝑓 = ◡ 𝑣 )
5	4	funeqd	⊢ ( 𝑓 = 𝑣 → ( Fun ◡ 𝑓 ↔ Fun ◡ 𝑣 ) )
6		sseq1	⊢ ( 𝑓 = 𝑣 → ( 𝑓 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑔 ) )
7		sseq2	⊢ ( 𝑓 = 𝑣 → ( 𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑣 ) )
8	6 7	orbi12d	⊢ ( 𝑓 = 𝑣 → ( ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ↔ ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) ) )
9	8	ralbidv	⊢ ( 𝑓 = 𝑣 → ( ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ↔ ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) ) )
10	5 9	anbi12d	⊢ ( 𝑓 = 𝑣 → ( ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ( Fun ◡ 𝑣 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) ) ) )
11	10	rspcv	⊢ ( 𝑣 ∈ 𝐴 → ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( Fun ◡ 𝑣 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) ) ) )
12		funeq	⊢ ( 𝑧 = ◡ 𝑣 → ( Fun 𝑧 ↔ Fun ◡ 𝑣 ) )
13	12	biimprcd	⊢ ( Fun ◡ 𝑣 → ( 𝑧 = ◡ 𝑣 → Fun 𝑧 ) )
14		sseq2	⊢ ( 𝑔 = 𝑥 → ( 𝑣 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑥 ) )
15		sseq1	⊢ ( 𝑔 = 𝑥 → ( 𝑔 ⊆ 𝑣 ↔ 𝑥 ⊆ 𝑣 ) )
16	14 15	orbi12d	⊢ ( 𝑔 = 𝑥 → ( ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) ↔ ( 𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣 ) ) )
17	16	rspcv	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) → ( 𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣 ) ) )
18		cnvss	⊢ ( 𝑣 ⊆ 𝑥 → ◡ 𝑣 ⊆ ◡ 𝑥 )
19		cnvss	⊢ ( 𝑥 ⊆ 𝑣 → ◡ 𝑥 ⊆ ◡ 𝑣 )
20	18 19	orim12i	⊢ ( ( 𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣 ) → ( ◡ 𝑣 ⊆ ◡ 𝑥 ∨ ◡ 𝑥 ⊆ ◡ 𝑣 ) )
21		sseq12	⊢ ( ( 𝑧 = ◡ 𝑣 ∧ 𝑤 = ◡ 𝑥 ) → ( 𝑧 ⊆ 𝑤 ↔ ◡ 𝑣 ⊆ ◡ 𝑥 ) )
22	21	ancoms	⊢ ( ( 𝑤 = ◡ 𝑥 ∧ 𝑧 = ◡ 𝑣 ) → ( 𝑧 ⊆ 𝑤 ↔ ◡ 𝑣 ⊆ ◡ 𝑥 ) )
23		sseq12	⊢ ( ( 𝑤 = ◡ 𝑥 ∧ 𝑧 = ◡ 𝑣 ) → ( 𝑤 ⊆ 𝑧 ↔ ◡ 𝑥 ⊆ ◡ 𝑣 ) )
24	22 23	orbi12d	⊢ ( ( 𝑤 = ◡ 𝑥 ∧ 𝑧 = ◡ 𝑣 ) → ( ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ↔ ( ◡ 𝑣 ⊆ ◡ 𝑥 ∨ ◡ 𝑥 ⊆ ◡ 𝑣 ) ) )
25	20 24	syl5ibrcom	⊢ ( ( 𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣 ) → ( ( 𝑤 = ◡ 𝑥 ∧ 𝑧 = ◡ 𝑣 ) → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) )
26	25	expd	⊢ ( ( 𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣 ) → ( 𝑤 = ◡ 𝑥 → ( 𝑧 = ◡ 𝑣 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) )
27	17 26	syl6com	⊢ ( ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = ◡ 𝑥 → ( 𝑧 = ◡ 𝑣 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
28	27	rexlimdv	⊢ ( ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 = ◡ 𝑣 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) )
29	28	com23	⊢ ( ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) → ( 𝑧 = ◡ 𝑣 → ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) )
30	29	alrimdv	⊢ ( ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) → ( 𝑧 = ◡ 𝑣 → ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) )
31	13 30	anim12ii	⊢ ( ( Fun ◡ 𝑣 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣 ) ) → ( 𝑧 = ◡ 𝑣 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
32	11 31	syl6com	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( 𝑣 ∈ 𝐴 → ( 𝑧 = ◡ 𝑣 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) ) )
33	32	rexlimdv	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( ∃ 𝑣 ∈ 𝐴 𝑧 = ◡ 𝑣 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
34	3 33	biimtrid	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
35	34	alrimiv	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
36		df-ral	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } → ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) )
37		vex	⊢ 𝑧 ∈ V
38		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ◡ 𝑥 ↔ 𝑧 = ◡ 𝑥 ) )
39	38	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 ) )
40	37 39	elab	⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 )
41		eqeq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 = ◡ 𝑥 ↔ 𝑤 = ◡ 𝑥 ) )
42	41	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 ) )
43	42	ralab	⊢ ( ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ↔ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) )
44	43	anbi2i	⊢ ( ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ↔ ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) )
45	40 44	imbi12i	⊢ ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } → ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
46	45	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } → ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) )
47	36 46	bitr2i	⊢ ( ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 = ◡ 𝑥 → ( Fun 𝑧 ∧ ∀ 𝑤 ( ∃ 𝑥 ∈ 𝐴 𝑤 = ◡ 𝑥 → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) ) ) ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) )
48	35 47	sylib	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) )
49		fununi	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( Fun 𝑧 ∧ ∀ 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) → Fun ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } )
50	48 49	syl	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } )
51		cnvuni	⊢ ◡ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡ 𝑥
52		vex	⊢ 𝑥 ∈ V
53	52	cnvex	⊢ ◡ 𝑥 ∈ V
54	53	dfiun2	⊢ ∪ 𝑥 ∈ 𝐴 ◡ 𝑥 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 }
55	51 54	eqtri	⊢ ◡ ∪ 𝐴 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 }
56	55	funeqi	⊢ ( Fun ◡ ∪ 𝐴 ↔ Fun ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ◡ 𝑥 } )
57	50 56	sylibr	⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ◡ ∪ 𝐴 )