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 ^◡ ∪ 𝐴 )

Metamath Proof Explorer

Theorem funcnvuni

Proof