Theorem funcnvuni 7119

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5958 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 5296	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ◡𝑥 = ◡𝑣)
2	1	eqeq2d 2632	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑧 = ◡𝑥 ↔ 𝑧 = ◡𝑣))
3	2	cbvrexv 3172	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 ↔ ∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣)
4		cnveq 5296	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ◡𝑓 = ◡𝑣)
5	4	funeqd 5910	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (Fun ◡𝑓 ↔ Fun ◡𝑣))
6		sseq1 3626	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑔))
7		sseq2 3627	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑣))
8	6, 7	orbi12d 746	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
9	8	ralbidv 2986	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
10	5, 9	anbi12d 747	. . . . . . . . 9 ⊢ (𝑓 = 𝑣 → ((Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
11	10	rspcv 3305	. . . . . . . 8 ⊢ (𝑣 ∈ 𝐴 → (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
12		funeq 5908	. . . . . . . . . 10 ⊢ (𝑧 = ◡𝑣 → (Fun 𝑧 ↔ Fun ◡𝑣))
13	12	biimprcd 240	. . . . . . . . 9 ⊢ (Fun ◡𝑣 → (𝑧 = ◡𝑣 → Fun 𝑧))
14		sseq2 3627	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑣 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑥))
15		sseq1 3626	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑔 ⊆ 𝑣 ↔ 𝑥 ⊆ 𝑣))
16	14, 15	orbi12d 746	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑥 → ((𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) ↔ (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
17	16	rspcv 3305	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
18		cnvss 5294	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ⊆ 𝑥 → ◡𝑣 ⊆ ◡𝑥)
19		cnvss 5294	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝑣 → ◡𝑥 ⊆ ◡𝑣)
20	18, 19	orim12i 538	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣))
21		sseq12 3628	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ◡𝑣 ∧ 𝑤 = ◡𝑥) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
22	21	ancoms 469	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
23		sseq12 3628	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑤 ⊆ 𝑧 ↔ ◡𝑥 ⊆ ◡𝑣))
24	22, 23	orbi12d 746	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → ((𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣)))
25	20, 24	syl5ibrcom 237	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
26	25	expd 452	. . . . . . . . . . . . 13 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
27	17, 26	syl6com 37	. . . . . . . . . . . 12 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑥 ∈ 𝐴 → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
28	27	rexlimdv 3030	. . . . . . . . . . 11 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
29	28	com23 86	. . . . . . . . . 10 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
30	29	alrimdv 1857	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
31	13, 30	anim12ii 594	. . . . . . . 8 ⊢ ((Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)) → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
32	11, 31	syl6com 37	. . . . . . 7 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (𝑣 ∈ 𝐴 → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))))
33	32	rexlimdv 3030	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
34	3, 33	syl5bi 232	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
35	34	alrimiv 1855	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
36		df-ral 2917	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
37		vex 3203	. . . . . . . 8 ⊢ 𝑧 ∈ V
38		eqeq1 2626	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = ◡𝑥 ↔ 𝑧 = ◡𝑥))
39	38	rexbidv 3052	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥))
40	37, 39	elab 3350	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥)
41		eqeq1 2626	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = ◡𝑥 ↔ 𝑤 = ◡𝑥))
42	41	rexbidv 3052	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥))
43	42	ralab 3367	. . . . . . . 8 ⊢ (∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
44	43	anbi2i 730	. . . . . . 7 ⊢ ((Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
45	40, 44	imbi12i 340	. . . . . 6 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
46	45	albii 1747	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
47	36, 46	bitr2i 265	. . . 4 ⊢ (∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))) ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
48	35, 47	sylib 208	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
49		fununi 5964	. . 3 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
50	48, 49	syl 17	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
51		cnvuni 5309	. . . 4 ⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
52		vex 3203	. . . . . 6 ⊢ 𝑥 ∈ V
53	52	cnvex 7113	. . . . 5 ⊢ ◡𝑥 ∈ V
54	53	dfiun2 4554	. . . 4 ⊢ ∪ 𝑥 ∈ 𝐴 ◡𝑥 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
55	51, 54	eqtri 2644	. . 3 ⊢ ◡∪ 𝐴 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
56	55	funeqi 5909	. 2 ⊢ (Fun ◡∪ 𝐴 ↔ Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
57	50, 56	sylibr 224	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384  ∀wal 1481   = wceq 1483   ∈ wcel 1990  {cab 2608  ∀wral 2912  ∃wrex 2913   ⊆ wss 3574  ∪ cuni 4436  ∪ ciun 4520  ^◡ccnv 5113  Fun wfun 5882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890

This theorem is referenced by:  fun11uni  7120