fununi

Description: The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004)

		Ref	Expression
	Assertion	fununi	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun f \to Rel f$
2	1	adantr	$⊢ (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Rel f$
3	2	ralimi	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall f \in A Rel f$
4		reluni	$⊢ Rel ⋃ A \leftrightarrow \forall f \in A Rel f$
5	3 4	sylibr	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Rel ⋃ A$
6		r19.28v	$⊢ (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f))$
7	6	ralimi	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f))$
8		ssel	$⊢ w \subseteq v \to (⟨x, y⟩ \in w \to ⟨x, y⟩ \in v)$
9	8	anim1d	$⊢ w \subseteq v \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to (⟨x, y⟩ \in v \land ⟨x, z⟩ \in v))$
10		dffun4	$⊢ Fun v \leftrightarrow (Rel v \land \forall x \forall y \forall z ((⟨x, y⟩ \in v \land ⟨x, z⟩ \in v) \to y = z))$
11	10	simprbi	$⊢ Fun v \to \forall x \forall y \forall z ((⟨x, y⟩ \in v \land ⟨x, z⟩ \in v) \to y = z)$
12	11	19.21bbi	$⊢ Fun v \to \forall z ((⟨x, y⟩ \in v \land ⟨x, z⟩ \in v) \to y = z)$
13	12	19.21bi	$⊢ Fun v \to ((⟨x, y⟩ \in v \land ⟨x, z⟩ \in v) \to y = z)$
14	9 13	syl9r	$⊢ Fun v \to (w \subseteq v \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
15	14	adantl	$⊢ (Fun w \land Fun v) \to (w \subseteq v \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
16		ssel	$⊢ v \subseteq w \to (⟨x, z⟩ \in v \to ⟨x, z⟩ \in w)$
17	16	anim2d	$⊢ v \subseteq w \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to (⟨x, y⟩ \in w \land ⟨x, z⟩ \in w))$
18		dffun4	$⊢ Fun w \leftrightarrow (Rel w \land \forall x \forall y \forall z ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in w) \to y = z))$
19	18	simprbi	$⊢ Fun w \to \forall x \forall y \forall z ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in w) \to y = z)$
20	19	19.21bbi	$⊢ Fun w \to \forall z ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in w) \to y = z)$
21	20	19.21bi	$⊢ Fun w \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in w) \to y = z)$
22	17 21	syl9r	$⊢ Fun w \to (v \subseteq w \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
23	22	adantr	$⊢ (Fun w \land Fun v) \to (v \subseteq w \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
24	15 23	jaod	$⊢ (Fun w \land Fun v) \to ((w \subseteq v \lor v \subseteq w) \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
25	24	imp	$⊢ ((Fun w \land Fun v) \land (w \subseteq v \lor v \subseteq w)) \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z)$
26	25	2ralimi	$⊢ \forall w \in A \forall v \in A ((Fun w \land Fun v) \land (w \subseteq v \lor v \subseteq w)) \to \forall w \in A \forall v \in A ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z)$
27		funeq	$⊢ f = w \to (Fun f \leftrightarrow Fun w)$
28		sseq1	$⊢ f = w \to (f \subseteq g \leftrightarrow w \subseteq g)$
29		sseq2	$⊢ f = w \to (g \subseteq f \leftrightarrow g \subseteq w)$
30	28 29	orbi12d	$⊢ f = w \to ((f \subseteq g \lor g \subseteq f) \leftrightarrow (w \subseteq g \lor g \subseteq w))$
31	27 30	anbi12d	$⊢ f = w \to ((Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow (Fun w \land (w \subseteq g \lor g \subseteq w)))$
32		sseq2	$⊢ g = v \to (w \subseteq g \leftrightarrow w \subseteq v)$
33		sseq1	$⊢ g = v \to (g \subseteq w \leftrightarrow v \subseteq w)$
34	32 33	orbi12d	$⊢ g = v \to ((w \subseteq g \lor g \subseteq w) \leftrightarrow (w \subseteq v \lor v \subseteq w))$
35	34	anbi2d	$⊢ g = v \to ((Fun w \land (w \subseteq g \lor g \subseteq w)) \leftrightarrow (Fun w \land (w \subseteq v \lor v \subseteq w)))$
36	31 35	cbvral2vw	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow \forall w \in A \forall v \in A (Fun w \land (w \subseteq v \lor v \subseteq w))$
37		ralcom	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow \forall g \in A \forall f \in A (Fun f \land (f \subseteq g \lor g \subseteq f))$
38		orcom	$⊢ (f \subseteq g \lor g \subseteq f) \leftrightarrow (g \subseteq f \lor f \subseteq g)$
39		sseq1	$⊢ g = w \to (g \subseteq f \leftrightarrow w \subseteq f)$
40		sseq2	$⊢ g = w \to (f \subseteq g \leftrightarrow f \subseteq w)$
41	39 40	orbi12d	$⊢ g = w \to ((g \subseteq f \lor f \subseteq g) \leftrightarrow (w \subseteq f \lor f \subseteq w))$
42	38 41	bitrid	$⊢ g = w \to ((f \subseteq g \lor g \subseteq f) \leftrightarrow (w \subseteq f \lor f \subseteq w))$
43	42	anbi2d	$⊢ g = w \to ((Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow (Fun f \land (w \subseteq f \lor f \subseteq w)))$
44		funeq	$⊢ f = v \to (Fun f \leftrightarrow Fun v)$
45		sseq2	$⊢ f = v \to (w \subseteq f \leftrightarrow w \subseteq v)$
46		sseq1	$⊢ f = v \to (f \subseteq w \leftrightarrow v \subseteq w)$
47	45 46	orbi12d	$⊢ f = v \to ((w \subseteq f \lor f \subseteq w) \leftrightarrow (w \subseteq v \lor v \subseteq w))$
48	44 47	anbi12d	$⊢ f = v \to ((Fun f \land (w \subseteq f \lor f \subseteq w)) \leftrightarrow (Fun v \land (w \subseteq v \lor v \subseteq w)))$
49	43 48	cbvral2vw	$⊢ \forall g \in A \forall f \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow \forall w \in A \forall v \in A (Fun v \land (w \subseteq v \lor v \subseteq w))$
50	37 49	bitri	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow \forall w \in A \forall v \in A (Fun v \land (w \subseteq v \lor v \subseteq w))$
51	36 50	anbi12i	$⊢ (\forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \land \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f))) \leftrightarrow (\forall w \in A \forall v \in A (Fun w \land (w \subseteq v \lor v \subseteq w)) \land \forall w \in A \forall v \in A (Fun v \land (w \subseteq v \lor v \subseteq w)))$
52		anidm	$⊢ (\forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \land \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f))) \leftrightarrow \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f))$
53		anandir	$⊢ ((Fun w \land Fun v) \land (w \subseteq v \lor v \subseteq w)) \leftrightarrow ((Fun w \land (w \subseteq v \lor v \subseteq w)) \land (Fun v \land (w \subseteq v \lor v \subseteq w)))$
54	53	2ralbii	$⊢ \forall w \in A \forall v \in A ((Fun w \land Fun v) \land (w \subseteq v \lor v \subseteq w)) \leftrightarrow \forall w \in A \forall v \in A ((Fun w \land (w \subseteq v \lor v \subseteq w)) \land (Fun v \land (w \subseteq v \lor v \subseteq w)))$
55		r19.26-2	$⊢ \forall w \in A \forall v \in A ((Fun w \land (w \subseteq v \lor v \subseteq w)) \land (Fun v \land (w \subseteq v \lor v \subseteq w))) \leftrightarrow (\forall w \in A \forall v \in A (Fun w \land (w \subseteq v \lor v \subseteq w)) \land \forall w \in A \forall v \in A (Fun v \land (w \subseteq v \lor v \subseteq w)))$
56	54 55	bitr2i	$⊢ (\forall w \in A \forall v \in A (Fun w \land (w \subseteq v \lor v \subseteq w)) \land \forall w \in A \forall v \in A (Fun v \land (w \subseteq v \lor v \subseteq w))) \leftrightarrow \forall w \in A \forall v \in A ((Fun w \land Fun v) \land (w \subseteq v \lor v \subseteq w))$
57	51 52 56	3bitr3i	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \leftrightarrow \forall w \in A \forall v \in A ((Fun w \land Fun v) \land (w \subseteq v \lor v \subseteq w))$
58		eluni	$⊢ ⟨x, y⟩ \in ⋃ A \leftrightarrow \exists w (⟨x, y⟩ \in w \land w \in A)$
59		eluni	$⊢ ⟨x, z⟩ \in ⋃ A \leftrightarrow \exists v (⟨x, z⟩ \in v \land v \in A)$
60	58 59	anbi12i	$⊢ (⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \leftrightarrow (\exists w (⟨x, y⟩ \in w \land w \in A) \land \exists v (⟨x, z⟩ \in v \land v \in A))$
61		exdistrv	$⊢ \exists w \exists v ((⟨x, y⟩ \in w \land w \in A) \land (⟨x, z⟩ \in v \land v \in A)) \leftrightarrow (\exists w (⟨x, y⟩ \in w \land w \in A) \land \exists v (⟨x, z⟩ \in v \land v \in A))$
62		an4	$⊢ ((⟨x, y⟩ \in w \land w \in A) \land (⟨x, z⟩ \in v \land v \in A)) \leftrightarrow ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \land (w \in A \land v \in A))$
63	62	biancomi	$⊢ ((⟨x, y⟩ \in w \land w \in A) \land (⟨x, z⟩ \in v \land v \in A)) \leftrightarrow ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v))$
64	63	2exbii	$⊢ \exists w \exists v ((⟨x, y⟩ \in w \land w \in A) \land (⟨x, z⟩ \in v \land v \in A)) \leftrightarrow \exists w \exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v))$
65	60 61 64	3bitr2i	$⊢ (⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \leftrightarrow \exists w \exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v))$
66	65	imbi1i	$⊢ ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z) \leftrightarrow (\exists w \exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z)$
67		19.23v	$⊢ \forall w (\exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z) \leftrightarrow (\exists w \exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z)$
68		r2al	$⊢ \forall w \in A \forall v \in A ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z) \leftrightarrow \forall w \forall v ((w \in A \land v \in A) \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
69		impexp	$⊢ (((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z) \leftrightarrow ((w \in A \land v \in A) \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
70	69	2albii	$⊢ \forall w \forall v (((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z) \leftrightarrow \forall w \forall v ((w \in A \land v \in A) \to ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z))$
71		19.23v	$⊢ \forall v (((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z) \leftrightarrow (\exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z)$
72	71	albii	$⊢ \forall w \forall v (((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z) \leftrightarrow \forall w (\exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z)$
73	68 70 72	3bitr2ri	$⊢ \forall w (\exists v ((w \in A \land v \in A) \land (⟨x, y⟩ \in w \land ⟨x, z⟩ \in v)) \to y = z) \leftrightarrow \forall w \in A \forall v \in A ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z)$
74	66 67 73	3bitr2i	$⊢ ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z) \leftrightarrow \forall w \in A \forall v \in A ((⟨x, y⟩ \in w \land ⟨x, z⟩ \in v) \to y = z)$
75	26 57 74	3imtr4i	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \to ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
76	75	alrimiv	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \to \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
77	76	alrimivv	$⊢ \forall f \in A \forall g \in A (Fun f \land (f \subseteq g \lor g \subseteq f)) \to \forall x \forall y \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
78	7 77	syl	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall x \forall y \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
79		dffun4	$⊢ Fun ⋃ A \leftrightarrow (Rel ⋃ A \land \forall x \forall y \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z))$
80	5 78 79	sylanbrc	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun ⋃ A$

Metamath Proof Explorer

Theorem fununi

Proof