Theorem funcnvuni 7868

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6570 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 5829	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ◡𝑥 = ◡𝑣)
2	1	eqeq2d 2747	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑧 = ◡𝑥 ↔ 𝑧 = ◡𝑣))
3	2	cbvrexvw 3226	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 ↔ ∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣)
4		cnveq 5829	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ◡𝑓 = ◡𝑣)
5	4	funeqd 6523	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (Fun ◡𝑓 ↔ Fun ◡𝑣))
6		sseq1 3969	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑔))
7		sseq2 3970	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑣 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑣))
8	6, 7	orbi12d 917	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑣 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
9	8	ralbidv 3174	. . . . . . . . . 10 ⊢ (𝑓 = 𝑣 → (∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)))
10	5, 9	anbi12d 631	. . . . . . . . 9 ⊢ (𝑓 = 𝑣 → ((Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
11	10	rspcv 3577	. . . . . . . 8 ⊢ (𝑣 ∈ 𝐴 → (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣))))
12		funeq 6521	. . . . . . . . . 10 ⊢ (𝑧 = ◡𝑣 → (Fun 𝑧 ↔ Fun ◡𝑣))
13	12	biimprcd 249	. . . . . . . . 9 ⊢ (Fun ◡𝑣 → (𝑧 = ◡𝑣 → Fun 𝑧))
14		sseq2 3970	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑣 ⊆ 𝑔 ↔ 𝑣 ⊆ 𝑥))
15		sseq1 3969	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑥 → (𝑔 ⊆ 𝑣 ↔ 𝑥 ⊆ 𝑣))
16	14, 15	orbi12d 917	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑥 → ((𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) ↔ (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
17	16	rspcv 3577	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣)))
18		cnvss 5828	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ⊆ 𝑥 → ◡𝑣 ⊆ ◡𝑥)
19		cnvss 5828	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝑣 → ◡𝑥 ⊆ ◡𝑣)
20	18, 19	orim12i 907	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣))
21		sseq12 3971	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ◡𝑣 ∧ 𝑤 = ◡𝑥) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
22	21	ancoms 459	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ↔ ◡𝑣 ⊆ ◡𝑥))
23		sseq12 3971	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑤 ⊆ 𝑧 ↔ ◡𝑥 ⊆ ◡𝑣))
24	22, 23	orbi12d 917	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → ((𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ (◡𝑣 ⊆ ◡𝑥 ∨ ◡𝑥 ⊆ ◡𝑣)))
25	20, 24	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → ((𝑤 = ◡𝑥 ∧ 𝑧 = ◡𝑣) → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
26	25	expd 416	. . . . . . . . . . . . 13 ⊢ ((𝑣 ⊆ 𝑥 ∨ 𝑥 ⊆ 𝑣) → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
27	17, 26	syl6com 37	. . . . . . . . . . . 12 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑥 ∈ 𝐴 → (𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
28	27	rexlimdv 3150	. . . . . . . . . . 11 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 = ◡𝑣 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
29	28	com23 86	. . . . . . . . . 10 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → (∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
30	29	alrimdv 1932	. . . . . . . . 9 ⊢ (∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣) → (𝑧 = ◡𝑣 → ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
31	13, 30	anim12ii 618	. . . . . . . 8 ⊢ ((Fun ◡𝑣 ∧ ∀𝑔 ∈ 𝐴 (𝑣 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑣)) → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
32	11, 31	syl6com 37	. . . . . . 7 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (𝑣 ∈ 𝐴 → (𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))))
33	32	rexlimdv 3150	. . . . . 6 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑣 ∈ 𝐴 𝑧 = ◡𝑣 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
34	3, 33	biimtrid 241	. . . . 5 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
35	34	alrimiv 1930	. . . 4 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
36		df-ral 3065	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
37		vex 3449	. . . . . . . 8 ⊢ 𝑧 ∈ V
38		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = ◡𝑥 ↔ 𝑧 = ◡𝑥))
39	38	rexbidv 3175	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥))
40	37, 39	elab 3630	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥)
41		eqeq1 2740	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = ◡𝑥 ↔ 𝑤 = ◡𝑥))
42	41	rexbidv 3175	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥))
43	42	ralab 3649	. . . . . . . 8 ⊢ (∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
44	43	anbi2i 623	. . . . . . 7 ⊢ ((Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) ↔ (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))))
45	40, 44	imbi12i 350	. . . . . 6 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ (∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
46	45	albii 1821	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} → (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧))) ↔ ∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))))
47	36, 46	bitr2i 275	. . . 4 ⊢ (∀𝑧(∃𝑥 ∈ 𝐴 𝑧 = ◡𝑥 → (Fun 𝑧 ∧ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 = ◡𝑥 → (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))) ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
48	35, 47	sylib 217	. . 3 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)))
49		fununi 6576	. . 3 ⊢ (∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (Fun 𝑧 ∧ ∀𝑤 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥} (𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
50	48, 49	syl 17	. 2 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
51		cnvuni 5842	. . . 4 ⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
52		vex 3449	. . . . . 6 ⊢ 𝑥 ∈ V
53	52	cnvex 7862	. . . . 5 ⊢ ◡𝑥 ∈ V
54	53	dfiun2 4993	. . . 4 ⊢ ∪ 𝑥 ∈ 𝐴 ◡𝑥 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
55	51, 54	eqtri 2764	. . 3 ⊢ ◡∪ 𝐴 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥}
56	55	funeqi 6522	. 2 ⊢ (Fun ◡∪ 𝐴 ↔ Fun ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = ◡𝑥})
57	50, 56	sylibr 233	1 ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845  ∀wal 1539   = wceq 1541   ∈ wcel 2106  {cab 2713  ∀wral 3064  ∃wrex 3073   ⊆ wss 3910  ∪ cuni 4865  ∪ ciun 4954  ^◡ccnv 5632  Fun wfun 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-fun 6498

This theorem is referenced by:  fun11uni  7869