Theorem fununi 2705

Description: The union of a chain (with respect to inclusion) of functions is a function.

Assertion

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

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

Proof of Theorem fununi

Step	Hyp	Ref	Expression
1		funrel 2681	. . . . . 6 ⊢ (Fun f → Rel f)
2	1	adantr 306	. . . . 5 ⊢ ((Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Rel f)
3	2	r19.20si 1254	. . . 4 ⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → ∀f ∈ A Rel f)
4		reluni 2493	. . . 4 ⊢ (Rel ∪A ↔ ∀f ∈ A Rel f)
5	3, 4	sylibr 175	. . 3 ⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Rel ∪A)
6		r19.28av 1294	. . . . 5 ⊢ ((Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)))
7	6	r19.20si 1254	. . . 4 ⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → ∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)))
8		ssel 1502	. . . . . . . . . . . . . 14 ⊢ (w ⊆ v → (⟨x, y⟩ ∈ w → ⟨x, y⟩ ∈ v))
9	8	anim1d 432	. . . . . . . . . . . . 13 ⊢ (w ⊆ v → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → (⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v)))
10		dffun4 2676	. . . . . . . . . . . . . . 15 ⊢ (Fun v ↔ (Rel v ∧ ∀x∀y∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z)))
11	10	pm3.27bd 263	. . . . . . . . . . . . . 14 ⊢ (Fun v → ∀x∀y∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z))
12		ax-4 673	. . . . . . . . . . . . . . 15 ⊢ (∀y∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z) → ∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z))
13	12	a4s 682	. . . . . . . . . . . . . 14 ⊢ (∀x∀y∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z) → ∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z))
14		ax-4 673	. . . . . . . . . . . . . 14 ⊢ (∀z((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z) → ((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z))
15	11, 13, 14	3syl 21	. . . . . . . . . . . . 13 ⊢ (Fun v → ((⟨x, y⟩ ∈ v ∧ ⟨x, z⟩ ∈ v) → y = z))
16	9, 15	syl9r 56	. . . . . . . . . . . 12 ⊢ (Fun v → (w ⊆ v → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
17	16	adantl 305	. . . . . . . . . . 11 ⊢ ((Fun w ∧ Fun v) → (w ⊆ v → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
18		ssel 1502	. . . . . . . . . . . . . 14 ⊢ (v ⊆ w → (⟨x, z⟩ ∈ v → ⟨x, z⟩ ∈ w))
19	18	anim2d 433	. . . . . . . . . . . . 13 ⊢ (v ⊆ w → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w)))
20		dffun4 2676	. . . . . . . . . . . . . . 15 ⊢ (Fun w ↔ (Rel w ∧ ∀x∀y∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z)))
21	20	pm3.27bd 263	. . . . . . . . . . . . . 14 ⊢ (Fun w → ∀x∀y∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z))
22		ax-4 673	. . . . . . . . . . . . . . 15 ⊢ (∀y∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z) → ∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z))
23	22	a4s 682	. . . . . . . . . . . . . 14 ⊢ (∀x∀y∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z) → ∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z))
24		ax-4 673	. . . . . . . . . . . . . 14 ⊢ (∀z((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z) → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z))
25	21, 23, 24	3syl 21	. . . . . . . . . . . . 13 ⊢ (Fun w → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ w) → y = z))
26	19, 25	syl9r 56	. . . . . . . . . . . 12 ⊢ (Fun w → (v ⊆ w → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
27	26	adantr 306	. . . . . . . . . . 11 ⊢ ((Fun w ∧ Fun v) → (v ⊆ w → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
28	17, 27	jaod 329	. . . . . . . . . 10 ⊢ ((Fun w ∧ Fun v) → ((w ⊆ v ∨ v ⊆ w) → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
29	28	imp 277	. . . . . . . . 9 ⊢ (((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)) → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z))
30	29	r19.20si 1254	. . . . . . . 8 ⊢ (∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)) → ∀v ∈ A ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z))
31	30	r19.20si 1254	. . . . . . 7 ⊢ (∀w ∈ A ∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)) → ∀w ∈ A ∀v ∈ A ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z))
32		funeq 2683	. . . . . . . . . . 11 ⊢ (f = w → (Fun f ↔ Fun w))
33		sseq1 1521	. . . . . . . . . . . 12 ⊢ (f = w → (f ⊆ g ↔ w ⊆ g))
34		sseq2 1522	. . . . . . . . . . . 12 ⊢ (f = w → (g ⊆ f ↔ g ⊆ w))
35	33, 34	orbi12d 475	. . . . . . . . . . 11 ⊢ (f = w → ((f ⊆ g ∨ g ⊆ f) ↔ (w ⊆ g ∨ g ⊆ w)))
36	32, 35	anbi12d 476	. . . . . . . . . 10 ⊢ (f = w → ((Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ (Fun w ∧ (w ⊆ g ∨ g ⊆ w))))
37		sseq2 1522	. . . . . . . . . . . 12 ⊢ (g = v → (w ⊆ g ↔ w ⊆ v))
38		sseq1 1521	. . . . . . . . . . . 12 ⊢ (g = v → (g ⊆ w ↔ v ⊆ w))
39	37, 38	orbi12d 475	. . . . . . . . . . 11 ⊢ (g = v → ((w ⊆ g ∨ g ⊆ w) ↔ (w ⊆ v ∨ v ⊆ w)))
40	39	anbi2d 468	. . . . . . . . . 10 ⊢ (g = v → ((Fun w ∧ (w ⊆ g ∨ g ⊆ w)) ↔ (Fun w ∧ (w ⊆ v ∨ v ⊆ w))))
41	36, 40	cbvral2v 1336	. . . . . . . . 9 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ ∀w ∈ A ∀v ∈ A (Fun w ∧ (w ⊆ v ∨ v ⊆ w)))
42		ralcom 1312	. . . . . . . . . 10 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ ∀g ∈ A ∀f ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)))
43		sseq1 1521	. . . . . . . . . . . . . 14 ⊢ (g = w → (g ⊆ f ↔ w ⊆ f))
44		sseq2 1522	. . . . . . . . . . . . . 14 ⊢ (g = w → (f ⊆ g ↔ f ⊆ w))
45	43, 44	orbi12d 475	. . . . . . . . . . . . 13 ⊢ (g = w → ((g ⊆ f ∨ f ⊆ g) ↔ (w ⊆ f ∨ f ⊆ w)))
46		orcom 209	. . . . . . . . . . . . 13 ⊢ ((f ⊆ g ∨ g ⊆ f) ↔ (g ⊆ f ∨ f ⊆ g))
47	45, 46	syl5bb 410	. . . . . . . . . . . 12 ⊢ (g = w → ((f ⊆ g ∨ g ⊆ f) ↔ (w ⊆ f ∨ f ⊆ w)))
48	47	anbi2d 468	. . . . . . . . . . 11 ⊢ (g = w → ((Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ (Fun f ∧ (w ⊆ f ∨ f ⊆ w))))
49		funeq 2683	. . . . . . . . . . . 12 ⊢ (f = v → (Fun f ↔ Fun v))
50		sseq2 1522	. . . . . . . . . . . . 13 ⊢ (f = v → (w ⊆ f ↔ w ⊆ v))
51		sseq1 1521	. . . . . . . . . . . . 13 ⊢ (f = v → (f ⊆ w ↔ v ⊆ w))
52	50, 51	orbi12d 475	. . . . . . . . . . . 12 ⊢ (f = v → ((w ⊆ f ∨ f ⊆ w) ↔ (w ⊆ v ∨ v ⊆ w)))
53	49, 52	anbi12d 476	. . . . . . . . . . 11 ⊢ (f = v → ((Fun f ∧ (w ⊆ f ∨ f ⊆ w)) ↔ (Fun v ∧ (w ⊆ v ∨ v ⊆ w))))
54	48, 53	cbvral2v 1336	. . . . . . . . . 10 ⊢ (∀g ∈ A ∀f ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆ v ∨ v ⊆ w)))
55	42, 54	bitr 151	. . . . . . . . 9 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆ v ∨ v ⊆ w)))
56	41, 55	anbi12i 369	. . . . . . . 8 ⊢ ((∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ∧ ∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f))) ↔ (∀w ∈ A ∀v ∈ A (Fun w ∧ (w ⊆ v ∨ v ⊆ w)) ∧ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆ v ∨ v ⊆ w))))
57		anidm 331	. . . . . . . 8 ⊢ ((∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ∧ ∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f))) ↔ ∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)))
58		anandir 393	. . . . . . . . . 10 ⊢ (((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)) ↔ ((Fun w ∧ (w ⊆ v ∨ v ⊆ w)) ∧ (Fun v ∧ (w ⊆ v ∨ v ⊆ w))))
59	58	bi2ral 1225	. . . . . . . . 9 ⊢ (∀w ∈ A ∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)) ↔ ∀w ∈ A ∀v ∈ A ((Fun w ∧ (w ⊆ v ∨ v ⊆ w)) ∧ (Fun v ∧ (w ⊆ v ∨ v ⊆ w))))
60		r19.26-2 1290	. . . . . . . . 9 ⊢ (∀w ∈ A ∀v ∈ A ((Fun w ∧ (w ⊆ v ∨ v ⊆ w)) ∧ (Fun v ∧ (w ⊆ v ∨ v ⊆ w))) ↔ (∀w ∈ A ∀v ∈ A (Fun w ∧ (w ⊆ v ∨ v ⊆ w)) ∧ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆ v ∨ v ⊆ w))))
61	59, 60	bitr2 152	. . . . . . . 8 ⊢ ((∀w ∈ A ∀v ∈ A (Fun w ∧ (w ⊆ v ∨ v ⊆ w)) ∧ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆ v ∨ v ⊆ w))) ↔ ∀w ∈ A ∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)))
62	56, 57, 61	3bitr3 156	. . . . . . 7 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) ↔ ∀w ∈ A ∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆ v ∨ v ⊆ w)))
63		eluni 1922	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ ∈ ∪A ↔ ∃w(⟨x, y⟩ ∈ w ∧ w ∈ A))
64		eluni 1922	. . . . . . . . . . 11 ⊢ (⟨x, z⟩ ∈ ∪A ↔ ∃v(⟨x, z⟩ ∈ v ∧ v ∈ A))
65	63, 64	anbi12i 369	. . . . . . . . . 10 ⊢ ((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) ↔ (∃w(⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ ∃v(⟨x, z⟩ ∈ v ∧ v ∈ A)))
66		eeanv 980	. . . . . . . . . . 11 ⊢ (∃w∃v((⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ (⟨x, z⟩ ∈ v ∧ v ∈ A)) ↔ (∃w(⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ ∃v(⟨x, z⟩ ∈ v ∧ v ∈ A)))
67		an4 388	. . . . . . . . . . . . 13 ⊢ (((⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ (⟨x, z⟩ ∈ v ∧ v ∈ A)) ↔ ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) ∧ (w ∈ A ∧ v ∈ A)))
68		ancom 333	. . . . . . . . . . . . 13 ⊢ (((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) ∧ (w ∈ A ∧ v ∈ A)) ↔ ((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)))
69	67, 68	bitr 151	. . . . . . . . . . . 12 ⊢ (((⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ (⟨x, z⟩ ∈ v ∧ v ∈ A)) ↔ ((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)))
70	69	bi2ex 734	. . . . . . . . . . 11 ⊢ (∃w∃v((⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ (⟨x, z⟩ ∈ v ∧ v ∈ A)) ↔ ∃w∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)))
71	66, 70	bitr3 153	. . . . . . . . . 10 ⊢ ((∃w(⟨x, y⟩ ∈ w ∧ w ∈ A) ∧ ∃v(⟨x, z⟩ ∈ v ∧ v ∈ A)) ↔ ∃w∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)))
72	65, 71	bitr 151	. . . . . . . . 9 ⊢ ((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) ↔ ∃w∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)))
73	72	imbi1i 161	. . . . . . . 8 ⊢ (((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z) ↔ (∃w∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z))
74		19.23v 950	. . . . . . . . . 10 ⊢ (∀v(((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ (∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z))
75	74	bial 695	. . . . . . . . 9 ⊢ (∀w∀v(((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ ∀w(∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z))
76		impexp 276	. . . . . . . . . . 11 ⊢ ((((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ ((w ∈ A ∧ v ∈ A) → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
77	76	bi2al 696	. . . . . . . . . 10 ⊢ (∀w∀v(((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ ∀w∀v((w ∈ A ∧ v ∈ A) → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
78		r2al 1231	. . . . . . . . . 10 ⊢ (∀w ∈ A ∀v ∈ A ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z) ↔ ∀w∀v((w ∈ A ∧ v ∈ A) → ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z)))
79	77, 78	bitr4 154	. . . . . . . . 9 ⊢ (∀w∀v(((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ ∀w ∈ A ∀v ∈ A ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z))
80		19.23v 950	. . . . . . . . 9 ⊢ (∀w(∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ (∃w∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z))
81	75, 79, 80	3bitr3r 157	. . . . . . . 8 ⊢ ((∃w∃v((w ∈ A ∧ v ∈ A) ∧ (⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v)) → y = z) ↔ ∀w ∈ A ∀v ∈ A ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z))
82	73, 81	bitr 151	. . . . . . 7 ⊢ (((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z) ↔ ∀w ∈ A ∀v ∈ A ((⟨x, y⟩ ∈ w ∧ ⟨x, z⟩ ∈ v) → y = z))
83	31, 62, 82	3imtr4 192	. . . . . 6 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) → ((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z))
84	83	19.21aiv 943	. . . . 5 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) → ∀z((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z))
85	84	19.21aivv 944	. . . 4 ⊢ (∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆ g ∨ g ⊆ f)) → ∀x∀y∀z((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z))
86	7, 85	syl 12	. . 3 ⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → ∀x∀y∀z((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z))
87	5, 86	jca 236	. 2 ⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (Rel ∪A ∧ ∀x∀y∀z((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z)))
88		dffun4 2676	. 2 ⊢ (Fun ∪A ↔ (Rel ∪A ∧ ∀x∀y∀z((⟨x, y⟩ ∈ ∪A ∧ ⟨x, z⟩ ∈ ∪A) → y = z)))
89	87, 88	sylibr 175	1 ⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ∪A)

Syntax hints:   → wi 2   ∨ wo 195   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wcel 1092  ∀wral 1201   ⊆ wss 1487  ⟨cop 1810  ∪cuni 1919  Rel wrel 2415  Fun wfun 2416

This theorem is referenced by:  funcnvuni 2706  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-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-br 2063  df-opab 2098  df-id 2125  df-rel 2425  df-cnv 2426  df-co 2427  df-fun 2432

metamath.org