Theorem funcnvuni 2706

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 2703 for "single-rooted" definition.)

Assertion

Ref	Expression
funcnvuni	⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ◡∪A)

Distinct variable group(s):   f,g,A

Proof of Theorem funcnvuni

Step	Hyp	Ref	Expression
1		cnveq 2513	. . . . . . . . . . 11 ⊢ (f = v → ◡f = ◡v)
2		funeq 2683	. . . . . . . . . . 11 ⊢ (◡f = ◡v → (Fun ◡f ↔ Fun ◡v))
3	1, 2	syl 12	. . . . . . . . . 10 ⊢ (f = v → (Fun ◡f ↔ Fun ◡v))
4		sseq1 1521	. . . . . . . . . . . 12 ⊢ (f = v → (f ⊆ g ↔ v ⊆ g))
5		sseq2 1522	. . . . . . . . . . . 12 ⊢ (f = v → (g ⊆ f ↔ g ⊆ v))
6	4, 5	orbi12d 475	. . . . . . . . . . 11 ⊢ (f = v → ((f ⊆ g ∨ g ⊆ f) ↔ (v ⊆ g ∨ g ⊆ v)))
7	6	biraldv 1219	. . . . . . . . . 10 ⊢ (f = v → (∀g ∈ A (f ⊆ g ∨ g ⊆ f) ↔ ∀g ∈ A (v ⊆ g ∨ g ⊆ v)))
8	3, 7	anbi12d 476	. . . . . . . . 9 ⊢ (f = v → ((Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) ↔ (Fun ◡v ∧ ∀g ∈ A (v ⊆ g ∨ g ⊆ v))))
9	8	rcla4v 1402	. . . . . . . 8 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (v ∈ A → (Fun ◡v ∧ ∀g ∈ A (v ⊆ g ∨ g ⊆ v))))
10		funeq 2683	. . . . . . . . . . 11 ⊢ (z = ◡v → (Fun z ↔ Fun ◡v))
11	10	biimprcd 138	. . . . . . . . . 10 ⊢ (Fun ◡v → (z = ◡v → Fun z))
12	11	adantr 306	. . . . . . . . 9 ⊢ ((Fun ◡v ∧ ∀g ∈ A (v ⊆ g ∨ g ⊆ v)) → (z = ◡v → Fun z))
13		sseq2 1522	. . . . . . . . . . . . . . . 16 ⊢ (g = x → (v ⊆ g ↔ v ⊆ x))
14		sseq1 1521	. . . . . . . . . . . . . . . 16 ⊢ (g = x → (g ⊆ v ↔ x ⊆ v))
15	13, 14	orbi12d 475	. . . . . . . . . . . . . . 15 ⊢ (g = x → ((v ⊆ g ∨ g ⊆ v) ↔ (v ⊆ x ∨ x ⊆ v)))
16	15	rcla4v 1402	. . . . . . . . . . . . . 14 ⊢ (∀g ∈ A (v ⊆ g ∨ g ⊆ v) → (x ∈ A → (v ⊆ x ∨ x ⊆ v)))
17		sseq12 1523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z = ◡v ∧ w = ◡x) → (z ⊆ w ↔ ◡v ⊆ ◡x))
18	17	ancoms 334	. . . . . . . . . . . . . . . . . 18 ⊢ ((w = ◡x ∧ z = ◡v) → (z ⊆ w ↔ ◡v ⊆ ◡x))
19		sseq12 1523	. . . . . . . . . . . . . . . . . 18 ⊢ ((w = ◡x ∧ z = ◡v) → (w ⊆ z ↔ ◡x ⊆ ◡v))
20	18, 19	orbi12d 475	. . . . . . . . . . . . . . . . 17 ⊢ ((w = ◡x ∧ z = ◡v) → ((z ⊆ w ∨ w ⊆ z) ↔ (◡v ⊆ ◡x ∨ ◡x ⊆ ◡v)))
21		cnvss 2512	. . . . . . . . . . . . . . . . . 18 ⊢ (v ⊆ x → ◡v ⊆ ◡x)
22		cnvss 2512	. . . . . . . . . . . . . . . . . 18 ⊢ (x ⊆ v → ◡x ⊆ ◡v)
23	21, 22	orim12i 271	. . . . . . . . . . . . . . . . 17 ⊢ ((v ⊆ x ∨ x ⊆ v) → (◡v ⊆ ◡x ∨ ◡x ⊆ ◡v))
24	20, 23	syl5bir 184	. . . . . . . . . . . . . . . 16 ⊢ ((w = ◡x ∧ z = ◡v) → ((v ⊆ x ∨ x ⊆ v) → (z ⊆ w ∨ w ⊆ z)))
25	24	com12 13	. . . . . . . . . . . . . . 15 ⊢ ((v ⊆ x ∨ x ⊆ v) → ((w = ◡x ∧ z = ◡v) → (z ⊆ w ∨ w ⊆ z)))
26	25	exp3a 292	. . . . . . . . . . . . . 14 ⊢ ((v ⊆ x ∨ x ⊆ v) → (w = ◡x → (z = ◡v → (z ⊆ w ∨ w ⊆ z))))
27	16, 26	syl6 23	. . . . . . . . . . . . 13 ⊢ (∀g ∈ A (v ⊆ g ∨ g ⊆ v) → (x ∈ A → (w = ◡x → (z = ◡v → (z ⊆ w ∨ w ⊆ z)))))
28	27	r19.23adv 1286	. . . . . . . . . . . 12 ⊢ (∀g ∈ A (v ⊆ g ∨ g ⊆ v) → (∃x ∈ A w = ◡x → (z = ◡v → (z ⊆ w ∨ w ⊆ z))))
29	28	com23 32	. . . . . . . . . . 11 ⊢ (∀g ∈ A (v ⊆ g ∨ g ⊆ v) → (z = ◡v → (∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z))))
30	29	19.21adv 945	. . . . . . . . . 10 ⊢ (∀g ∈ A (v ⊆ g ∨ g ⊆ v) → (z = ◡v → ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z))))
31	30	adantl 305	. . . . . . . . 9 ⊢ ((Fun ◡v ∧ ∀g ∈ A (v ⊆ g ∨ g ⊆ v)) → (z = ◡v → ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z))))
32	12, 31	jcad 455	. . . . . . . 8 ⊢ ((Fun ◡v ∧ ∀g ∈ A (v ⊆ g ∨ g ⊆ v)) → (z = ◡v → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))))
33	9, 32	syl6 23	. . . . . . 7 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (v ∈ A → (z = ◡v → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z))))))
34	33	r19.23adv 1286	. . . . . 6 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (∃v ∈ A z = ◡v → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))))
35		cnveq 2513	. . . . . . . 8 ⊢ (x = v → ◡x = ◡v)
36	35	cleq2d 1112	. . . . . . 7 ⊢ (x = v → (z = ◡x ↔ z = ◡v))
37	36	cbvrexv 1334	. . . . . 6 ⊢ (∃x ∈ A z = ◡x ↔ ∃v ∈ A z = ◡v)
38	34, 37	syl5ib 181	. . . . 5 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (∃x ∈ A z = ◡x → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))))
39	38	19.21aiv 943	. . . 4 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → ∀z(∃x ∈ A z = ◡x → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))))
40		df-ral 1205	. . . . 5 ⊢ (∀z ∈ {y∣∃x ∈ A y = ◡x} (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z)) ↔ ∀z(z ∈ {y∣∃x ∈ A y = ◡x} → (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z))))
41		visset 1350	. . . . . . . 8 ⊢ z ∈ V
42		cleq1 1107	. . . . . . . . 9 ⊢ (y = z → (y = ◡x ↔ z = ◡x))
43	42	birexdv 1220	. . . . . . . 8 ⊢ (y = z → (∃x ∈ A y = ◡x ↔ ∃x ∈ A z = ◡x))
44	41, 43	elab 1415	. . . . . . 7 ⊢ (z ∈ {y∣∃x ∈ A y = ◡x} ↔ ∃x ∈ A z = ◡x)
45		df-ral 1205	. . . . . . . . 9 ⊢ (∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z) ↔ ∀w(w ∈ {y∣∃x ∈ A y = ◡x} → (z ⊆ w ∨ w ⊆ z)))
46		visset 1350	. . . . . . . . . . . 12 ⊢ w ∈ V
47		cleq1 1107	. . . . . . . . . . . . 13 ⊢ (y = w → (y = ◡x ↔ w = ◡x))
48	47	birexdv 1220	. . . . . . . . . . . 12 ⊢ (y = w → (∃x ∈ A y = ◡x ↔ ∃x ∈ A w = ◡x))
49	46, 48	elab 1415	. . . . . . . . . . 11 ⊢ (w ∈ {y∣∃x ∈ A y = ◡x} ↔ ∃x ∈ A w = ◡x)
50	49	imbi1i 161	. . . . . . . . . 10 ⊢ ((w ∈ {y∣∃x ∈ A y = ◡x} → (z ⊆ w ∨ w ⊆ z)) ↔ (∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))
51	50	bial 695	. . . . . . . . 9 ⊢ (∀w(w ∈ {y∣∃x ∈ A y = ◡x} → (z ⊆ w ∨ w ⊆ z)) ↔ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))
52	45, 51	bitr 151	. . . . . . . 8 ⊢ (∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z) ↔ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))
53	52	anbi2i 367	. . . . . . 7 ⊢ ((Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z)) ↔ (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z))))
54	44, 53	imbi12i 163	. . . . . 6 ⊢ ((z ∈ {y∣∃x ∈ A y = ◡x} → (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z))) ↔ (∃x ∈ A z = ◡x → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))))
55	54	bial 695	. . . . 5 ⊢ (∀z(z ∈ {y∣∃x ∈ A y = ◡x} → (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z))) ↔ ∀z(∃x ∈ A z = ◡x → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))))
56	40, 55	bitr2 152	. . . 4 ⊢ (∀z(∃x ∈ A z = ◡x → (Fun z ∧ ∀w(∃x ∈ A w = ◡x → (z ⊆ w ∨ w ⊆ z)))) ↔ ∀z ∈ {y∣∃x ∈ A y = ◡x} (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z)))
57	39, 56	sylib 173	. . 3 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → ∀z ∈ {y∣∃x ∈ A y = ◡x} (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z)))
58		fununi 2705	. . 3 ⊢ (∀z ∈ {y∣∃x ∈ A y = ◡x} (Fun z ∧ ∀w ∈ {y∣∃x ∈ A y = ◡x} (z ⊆ w ∨ w ⊆ z)) → Fun ∪{y∣∃x ∈ A y = ◡x})
59	57, 58	syl 12	. 2 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ ft/I>)) → Fun ∪{y∣∃x ∈ A y = ◡x})
60		cnvuni 2521	. . . 4 ⊢ ◡∪A = ∪x ∈ A ◡x
61		visset 1350	. . . . . 6 ⊢ x ∈ V
62	61	cnvex 2670	. . . . 5 ⊢ ◡x ∈ V
63	62	dfiun2 2014	. . . 4 ⊢ ∪x ∈ A ◡x = ∪{y∣∃x ∈ A y = ◡x}
64	60, 63	eqtr 1119	. . 3 ⊢ ◡∪A = ∪{y∣∃x ∈ A y = ◡x}
65		funeq 2683	. . 3 ⊢ (◡∪A = ∪{y∣∃x ∈ A y = ◡x} → (Fun ◡∪A ↔ Fun ∪{y∣∃x ∈ A y = ◡x}))
66	64, 65	ax-mp 6	. 2 ⊢ (Fun ◡∪A ↔ Fun ∪{y∣∃x ∈ A y = ◡x})
67	59, 66	sylibr 175	1 ⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ◡∪A)

Syntax hints:   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∀wal 672   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202   ⊆ wss 1487  ∪cuni 1919  ∪ciun 1994  ^◡ccnv 2409  Fun wfun 2416

This theorem is referenced by:  fun11uni 2707

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-iun 1996  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-fun 2432

metamath.org