Theorem funcnvuni 5390

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5382 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 4896	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ◡𝑥 = ◡𝑣)
2	1	eqeq2d 2241	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑧 = ◡𝑥 ↔ 𝑧 = ◡𝑣))
3	2	cbvrexv 2766	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 ↔ ∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣)
4		cnveq 4896	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ◡𝑓 = ◡𝑣)
5	4	funeqd 5340	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (Fun ◡𝑓 ↔ Fun ◡𝑣))
6		sseq1 3247	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑔))
7		sseq2 3248	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑣))
8	6, 7	orbi12d 798	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
9	8	ralbidv 2530	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
10	5, 9	anbi12d 473	. . . . . . . . 9 ⊢ (𝑓 = 𝑣 → ((Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
11	10	rspcv 2903	. . . . . . . 8 ⊢ (𝑣 ∈ 𝐴 → (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
12		funeq 5338	. . . . . . . . . 10 ⊢ (𝑧 = ◡𝑣 → (Fun 𝑧 ↔ Fun ◡𝑣))
13	12	biimprcd 160	. . . . . . . . 9 ⊢ (Fun ◡𝑣 → (𝑧 = ◡𝑣 → Fun 𝑧))
14		sseq2 3248	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑣 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑥))
15		sseq1 3247	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑔 ⊆ 𝑣 ↔ 𝑥 ⊆ 𝑣))
16	14, 15	orbi12d 798	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑥 → ((𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) ↔ (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
17	16	rspcv 2903	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
18		cnvss 4895	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ⊆ 𝑥 → ◡𝑣 ⊆ ◡𝑥)
19		cnvss 4895	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝑣 → ◡𝑥 ⊆ ◡𝑣)
20	18, 19	orim12i 764	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣))
21		sseq12 3249	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ◡𝑣 ∧ 𝑤 = ◡𝑥) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
22	21	ancoms 268	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
23		sseq12 3249	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑤 ⊆ 𝑧 ↔ ◡𝑥 ⊆ ◡𝑣))
24	22, 23	orbi12d 798	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → ((𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣)))
25	20, 24	syl5ibrcom 157	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
26	25	expd 258	. . . . . . . . . . . . 13 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
27	17, 26	syl6com 35	. . . . . . . . . . . 12 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑥 ∈ 𝐴 → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
28	27	rexlimdv 2647	. . . . . . . . . . 11 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
29	28	com23 78	. . . . . . . . . 10 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
30	29	alrimdv 1922	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
31	13, 30	anim12ii 343	. . . . . . . 8 ⊢ ((Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)) → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
32	11, 31	syl6com 35	. . . . . . 7 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (𝑣 ∈ 𝐴 → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))))
33	32	rexlimdv 2647	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
34	3, 33	biimtrid 152	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
35	34	alrimiv 1920	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
36		df-ral 2513	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
37		vex 2802	. . . . . . . 8 ⊢ 𝑧 ∈ V
38		eqeq1 2236	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = ◡𝑥 ↔ 𝑧 = ◡𝑥))
39	38	rexbidv 2531	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥))
40	37, 39	elab 2947	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥)
41		eqeq1 2236	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = ◡𝑥 ↔ 𝑤 = ◡𝑥))
42	41	rexbidv 2531	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥))
43	42	ralab 2963	. . . . . . . 8 ⊢ (∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
44	43	anbi2i 457	. . . . . . 7 ⊢ ((Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
45	40, 44	imbi12i 239	. . . . . 6 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
46	45	albii 1516	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
47	36, 46	bitr2i 185	. . . 4 ⊢ (∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))) ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
48	35, 47	sylib 122	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
49		fununi 5389	. . 3 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
50	48, 49	syl 14	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
51		cnvuni 4908	. . . 4 ⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
52		vex 2802	. . . . . 6 ⊢ 𝑥 ∈ V
53	52	cnvex 5267	. . . . 5 ⊢ ◡𝑥 ∈ V
54	53	dfiun2 3999	. . . 4 ⊢ ∪ 𝑥 ∈ 𝐴 ◡𝑥 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
55	51, 54	eqtri 2250	. . 3 ⊢ ◡∪ 𝐴 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
56	55	funeqi 5339	. 2 ⊢ (Fun ◡∪ 𝐴 ↔ Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
57	50, 56	sylibr 134	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 713  ∀wal 1393   = wceq 1395   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∃wrex 2509   ⊆ wss 3197  ∪ cuni 3888  ∪ ciun 3965  ^◡ccnv 4718  Fun wfun 5312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-iun 3967  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-fun 5320

This theorem is referenced by:  fun11uni  5391