Theorem funcnvuni 7968

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

Assertion

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

Distinct variable group:   𝑓,𝑔,𝐴

Proof of Theorem funcnvuni

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnveq 5858	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ◡𝑥 = ◡𝑣)
2	1	eqeq2d 2774	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑧 = ◡𝑥 ↔ 𝑧 = ◡𝑣))
3	2	cbvrexvw 3245	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 ↔ ∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣)
4		cnveq 5858	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ◡𝑓 = ◡𝑣)
5	4	funeqd 6581	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (Fun ◡𝑓 ↔ Fun ◡𝑣))
6		sseq1 3938	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑔))
7		sseq2 3939	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑣))
8	6, 7	orbi12d 932	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
9	8	ralbidv 3189	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
10	5, 9	anbi12d 644	. . . . . . . . 9 ⊢ (𝑓 = 𝑣 → ((Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
11	10	rspcv 3576	. . . . . . . 8 ⊢ (𝑣 ∈ 𝐴 → (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
12		funeq 6579	. . . . . . . . . 10 ⊢ (𝑧 = ◡𝑣 → (Fun 𝑧 ↔ Fun ◡𝑣))
13	12	biimprcd 253	. . . . . . . . 9 ⊢ (Fun ◡𝑣 → (𝑧 = ◡𝑣 → Fun 𝑧))
14		sseq2 3939	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑣 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑥))
15		sseq1 3938	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑔 ⊆ 𝑣 ↔ 𝑥 ⊆ 𝑣))
16	14, 15	orbi12d 932	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑥 → ((𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) ↔ (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
17	16	rspcv 3576	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
18		cnvss 5857	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ⊆ 𝑥 → ◡𝑣 ⊆ ◡𝑥)
19		cnvss 5857	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝑣 → ◡𝑥 ⊆ ◡𝑣)
20	18, 19	orim12i 922	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣))
21		sseq12 3940	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ◡𝑣 ∧ 𝑤 = ◡𝑥) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
22	21	ancoms 464	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
23		sseq12 3940	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑤 ⊆ 𝑧 ↔ ◡𝑥 ⊆ ◡𝑣))
24	22, 23	orbi12d 932	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → ((𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣)))
25	20, 24	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
26	25	expd 421	. . . . . . . . . . . . 13 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
27	17, 26	syl6com 38	. . . . . . . . . . . 12 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑥 ∈ 𝐴 → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
28	27	rexlimdv 3165	. . . . . . . . . . 11 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
29	28	com23 87	. . . . . . . . . 10 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
30	29	alrimdv 1964	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
31	13, 30	anim12ii 630	. . . . . . . 8 ⊢ ((Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)) → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
32	11, 31	syl6com 38	. . . . . . 7 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (𝑣 ∈ 𝐴 → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))))
33	32	rexlimdv 3165	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
34	3, 33	biimtrid 245	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
35	34	alrimiv 1962	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
36		df-ral 3081	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
37		vex 3458	. . . . . . . 8 ⊢ 𝑧 ∈ V
38		eqeq1 2767	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = ◡𝑥 ↔ 𝑧 = ◡𝑥))
39	38	rexbidv 3190	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥))
40	37, 39	elab 3636	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥)
41		eqeq1 2767	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = ◡𝑥 ↔ 𝑤 = ◡𝑥))
42	41	rexbidv 3190	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥))
43	42	ralab 3654	. . . . . . . 8 ⊢ (∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
44	43	anbi2i 635	. . . . . . 7 ⊢ ((Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
45	40, 44	imbi12i 353	. . . . . 6 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
46	45	albii 1852	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
47	36, 46	bitr2i 279	. . . 4 ⊢ (∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))) ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
48	35, 47	sylib 221	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
49		fununi 6637	. . 3 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
50	48, 49	syl 18	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
51		cnvuni 5875	. . . 4 ⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
52		vex 3458	. . . . . 6 ⊢ 𝑥 ∈ V
53	52	cnvex 7961	. . . . 5 ⊢ ◡𝑥 ∈ V
54	53	dfiun2 4993	. . . 4 ⊢ ∪ 𝑥 ∈ 𝐴 ◡𝑥 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
55	51, 54	eqtri 2786	. . 3 ⊢ ◡∪ 𝐴 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
56	55	funeqi 6580	. 2 ⊢ (Fun ◡∪ 𝐴 ↔ Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
57	50, 56	sylibr 237	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570   ∈ wcel 2147  {cab 2741  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900  ∪ cuni 4870  ∪ ciun 4954  ^◡ccnv 5654  Fun wfun 6552

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6560

This theorem is used by:  fun11uni  7969