funcnvuni

Description: The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004)

		Ref	Expression
	Assertion	funcnvuni	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun {⋃ A}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		cnveq	$⊢ x = v \to x^{-1} = v^{-1}$
2	1	eqeq2d	$⊢ x = v \to (z = x^{-1} \leftrightarrow z = v^{-1})$
3	2	cbvrexvw	$⊢ \exists x \in A z = x^{-1} \leftrightarrow \exists v \in A z = v^{-1}$
4		cnveq	$⊢ f = v \to f^{-1} = v^{-1}$
5	4	funeqd	$⊢ f = v \to (Fun f^{-1} \leftrightarrow Fun v^{-1})$
6		sseq1	$⊢ f = v \to (f \subseteq g \leftrightarrow v \subseteq g)$
7		sseq2	$⊢ f = v \to (g \subseteq f \leftrightarrow g \subseteq v)$
8	6 7	orbi12d	$⊢ f = v \to ((f \subseteq g \lor g \subseteq f) \leftrightarrow (v \subseteq g \lor g \subseteq v))$
9	8	ralbidv	$⊢ f = v \to (\forall g \in A (f \subseteq g \lor g \subseteq f) \leftrightarrow \forall g \in A (v \subseteq g \lor g \subseteq v))$
10	5 9	anbi12d	$⊢ f = v \to ((Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \leftrightarrow (Fun v^{-1} \land \forall g \in A (v \subseteq g \lor g \subseteq v)))$
11	10	rspcv	$⊢ v \in A \to (\forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (Fun v^{-1} \land \forall g \in A (v \subseteq g \lor g \subseteq v)))$
12		funeq	$⊢ z = v^{-1} \to (Fun z \leftrightarrow Fun v^{-1})$
13	12	biimprcd	$⊢ Fun v^{-1} \to (z = v^{-1} \to Fun z)$
14		sseq2	$⊢ g = x \to (v \subseteq g \leftrightarrow v \subseteq x)$
15		sseq1	$⊢ g = x \to (g \subseteq v \leftrightarrow x \subseteq v)$
16	14 15	orbi12d	$⊢ g = x \to ((v \subseteq g \lor g \subseteq v) \leftrightarrow (v \subseteq x \lor x \subseteq v))$
17	16	rspcv	$⊢ x \in A \to (\forall g \in A (v \subseteq g \lor g \subseteq v) \to (v \subseteq x \lor x \subseteq v))$
18		cnvss	$⊢ v \subseteq x \to v^{-1} \subseteq x^{-1}$
19		cnvss	$⊢ x \subseteq v \to x^{-1} \subseteq v^{-1}$
20	18 19	orim12i	$⊢ (v \subseteq x \lor x \subseteq v) \to (v^{-1} \subseteq x^{-1} \lor x^{-1} \subseteq v^{-1})$
21		sseq12	$⊢ (z = v^{-1} \land w = x^{-1}) \to (z \subseteq w \leftrightarrow v^{-1} \subseteq x^{-1})$
22	21	ancoms	$⊢ (w = x^{-1} \land z = v^{-1}) \to (z \subseteq w \leftrightarrow v^{-1} \subseteq x^{-1})$
23		sseq12	$⊢ (w = x^{-1} \land z = v^{-1}) \to (w \subseteq z \leftrightarrow x^{-1} \subseteq v^{-1})$
24	22 23	orbi12d	$⊢ (w = x^{-1} \land z = v^{-1}) \to ((z \subseteq w \lor w \subseteq z) \leftrightarrow (v^{-1} \subseteq x^{-1} \lor x^{-1} \subseteq v^{-1}))$
25	20 24	syl5ibrcom	$⊢ (v \subseteq x \lor x \subseteq v) \to ((w = x^{-1} \land z = v^{-1}) \to (z \subseteq w \lor w \subseteq z))$
26	25	expd	$⊢ (v \subseteq x \lor x \subseteq v) \to (w = x^{-1} \to (z = v^{-1} \to (z \subseteq w \lor w \subseteq z)))$
27	17 26	syl6com	$⊢ \forall g \in A (v \subseteq g \lor g \subseteq v) \to (x \in A \to (w = x^{-1} \to (z = v^{-1} \to (z \subseteq w \lor w \subseteq z))))$
28	27	rexlimdv	$⊢ \forall g \in A (v \subseteq g \lor g \subseteq v) \to (\exists x \in A w = x^{-1} \to (z = v^{-1} \to (z \subseteq w \lor w \subseteq z)))$
29	28	com23	$⊢ \forall g \in A (v \subseteq g \lor g \subseteq v) \to (z = v^{-1} \to (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z)))$
30	29	alrimdv	$⊢ \forall g \in A (v \subseteq g \lor g \subseteq v) \to (z = v^{-1} \to \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z)))$
31	13 30	anim12ii	$⊢ (Fun v^{-1} \land \forall g \in A (v \subseteq g \lor g \subseteq v)) \to (z = v^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))))$
32	11 31	syl6com	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (v \in A \to (z = v^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z)))))$
33	32	rexlimdv	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (\exists v \in A z = v^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))))$
34	3 33	biimtrid	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (\exists x \in A z = x^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))))$
35	34	alrimiv	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall z (\exists x \in A z = x^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))))$
36		df-ral	$⊢ \forall z \in \{y \| \exists x \in A y = x^{-1}\} (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z)) \leftrightarrow \forall z (z \in \{y \| \exists x \in A y = x^{-1}\} \to (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z)))$
37		vex	$⊢ z \in V$
38		eqeq1	$⊢ y = z \to (y = x^{-1} \leftrightarrow z = x^{-1})$
39	38	rexbidv	$⊢ y = z \to (\exists x \in A y = x^{-1} \leftrightarrow \exists x \in A z = x^{-1})$
40	37 39	elab	$⊢ z \in \{y \| \exists x \in A y = x^{-1}\} \leftrightarrow \exists x \in A z = x^{-1}$
41		eqeq1	$⊢ y = w \to (y = x^{-1} \leftrightarrow w = x^{-1})$
42	41	rexbidv	$⊢ y = w \to (\exists x \in A y = x^{-1} \leftrightarrow \exists x \in A w = x^{-1})$
43	42	ralab	$⊢ \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z) \leftrightarrow \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))$
44	43	anbi2i	$⊢ (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z)) \leftrightarrow (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z)))$
45	40 44	imbi12i	$⊢ (z \in \{y \| \exists x \in A y = x^{-1}\} \to (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z))) \leftrightarrow (\exists x \in A z = x^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))))$
46	45	albii	$⊢ \forall z (z \in \{y \| \exists x \in A y = x^{-1}\} \to (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z))) \leftrightarrow \forall z (\exists x \in A z = x^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z))))$
47	36 46	bitr2i	$⊢ \forall z (\exists x \in A z = x^{-1} \to (Fun z \land \forall w (\exists x \in A w = x^{-1} \to (z \subseteq w \lor w \subseteq z)))) \leftrightarrow \forall z \in \{y \| \exists x \in A y = x^{-1}\} (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z))$
48	35 47	sylib	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall z \in \{y \| \exists x \in A y = x^{-1}\} (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z))$
49		fununi	$⊢ \forall z \in \{y \| \exists x \in A y = x^{-1}\} (Fun z \land \forall w \in \{y \| \exists x \in A y = x^{-1}\} (z \subseteq w \lor w \subseteq z)) \to Fun ⋃ \{y \| \exists x \in A y = x^{-1}\}$
50	48 49	syl	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun ⋃ \{y \| \exists x \in A y = x^{-1}\}$
51		cnvuni	$⊢ {⋃ A}^{-1} = ⋃_{x \in A} x^{-1}$
52		vex	$⊢ x \in V$
53	52	cnvex	$⊢ x^{-1} \in V$
54	53	dfiun2	$⊢ ⋃_{x \in A} x^{-1} = ⋃ \{y \| \exists x \in A y = x^{-1}\}$
55	51 54	eqtri	$⊢ {⋃ A}^{-1} = ⋃ \{y \| \exists x \in A y = x^{-1}\}$
56	55	funeqi	$⊢ Fun {⋃ A}^{-1} \leftrightarrow Fun ⋃ \{y \| \exists x \in A y = x^{-1}\}$
57	50 56	sylibr	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun {⋃ A}^{-1}$

Metamath Proof Explorer

Theorem funcnvuni

Proof