Theorem funcnvuni 7921

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6611 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 5867	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ◡𝑥 = ◡𝑣)
2	1	eqeq2d 2737	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑧 = ◡𝑥 ↔ 𝑧 = ◡𝑣))
3	2	cbvrexvw 3229	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 ↔ ∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣)
4		cnveq 5867	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ◡𝑓 = ◡𝑣)
5	4	funeqd 6564	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (Fun ◡𝑓 ↔ Fun ◡𝑣))
6		sseq1 4002	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑔))
7		sseq2 4003	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑣))
8	6, 7	orbi12d 915	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
9	8	ralbidv 3171	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
10	5, 9	anbi12d 630	. . . . . . . . 9 ⊢ (𝑓 = 𝑣 → ((Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
11	10	rspcv 3602	. . . . . . . 8 ⊢ (𝑣 ∈ 𝐴 → (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
12		funeq 6562	. . . . . . . . . 10 ⊢ (𝑧 = ◡𝑣 → (Fun 𝑧 ↔ Fun ◡𝑣))
13	12	biimprcd 249	. . . . . . . . 9 ⊢ (Fun ◡𝑣 → (𝑧 = ◡𝑣 → Fun 𝑧))
14		sseq2 4003	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑣 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑥))
15		sseq1 4002	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑔 ⊆ 𝑣 ↔ 𝑥 ⊆ 𝑣))
16	14, 15	orbi12d 915	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑥 → ((𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) ↔ (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
17	16	rspcv 3602	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
18		cnvss 5866	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ⊆ 𝑥 → ◡𝑣 ⊆ ◡𝑥)
19		cnvss 5866	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝑣 → ◡𝑥 ⊆ ◡𝑣)
20	18, 19	orim12i 905	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣))
21		sseq12 4004	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ◡𝑣 ∧ 𝑤 = ◡𝑥) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
22	21	ancoms 458	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
23		sseq12 4004	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑤 ⊆ 𝑧 ↔ ◡𝑥 ⊆ ◡𝑣))
24	22, 23	orbi12d 915	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → ((𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣)))
25	20, 24	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
26	25	expd 415	. . . . . . . . . . . . 13 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
27	17, 26	syl6com 37	. . . . . . . . . . . 12 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑥 ∈ 𝐴 → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
28	27	rexlimdv 3147	. . . . . . . . . . 11 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
29	28	com23 86	. . . . . . . . . 10 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
30	29	alrimdv 1924	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
31	13, 30	anim12ii 617	. . . . . . . 8 ⊢ ((Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)) → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
32	11, 31	syl6com 37	. . . . . . 7 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (𝑣 ∈ 𝐴 → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))))
33	32	rexlimdv 3147	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
34	3, 33	biimtrid 241	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
35	34	alrimiv 1922	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
36		df-ral 3056	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
37		vex 3472	. . . . . . . 8 ⊢ 𝑧 ∈ V
38		eqeq1 2730	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = ◡𝑥 ↔ 𝑧 = ◡𝑥))
39	38	rexbidv 3172	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥))
40	37, 39	elab 3663	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥)
41		eqeq1 2730	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = ◡𝑥 ↔ 𝑤 = ◡𝑥))
42	41	rexbidv 3172	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥))
43	42	ralab 3682	. . . . . . . 8 ⊢ (∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
44	43	anbi2i 622	. . . . . . 7 ⊢ ((Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
45	40, 44	imbi12i 350	. . . . . 6 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
46	45	albii 1813	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
47	36, 46	bitr2i 276	. . . 4 ⊢ (∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))) ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
48	35, 47	sylib 217	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
49		fununi 6617	. . 3 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
50	48, 49	syl 17	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
51		cnvuni 5880	. . . 4 ⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
52		vex 3472	. . . . . 6 ⊢ 𝑥 ∈ V
53	52	cnvex 7915	. . . . 5 ⊢ ◡𝑥 ∈ V
54	53	dfiun2 5029	. . . 4 ⊢ ∪ 𝑥 ∈ 𝐴 ◡𝑥 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
55	51, 54	eqtri 2754	. . 3 ⊢ ◡∪ 𝐴 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
56	55	funeqi 6563	. 2 ⊢ (Fun ◡∪ 𝐴 ↔ Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
57	50, 56	sylibr 233	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844  ∀wal 1531   = wceq 1533   ∈ wcel 2098  {cab 2703  ∀wral 3055  ∃wrex 3064   ⊆ wss 3943  ∪ cuni 4902  ∪ ciun 4990  ^◡ccnv 5668  Fun wfun 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-fun 6539

This theorem is referenced by:  fun11uni  7922