fmucnd

Description: The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of BourbakiTop1 p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017)

	Ref	Expression
Hypotheses	fmucnd.1	$⊢ φ \to U \in UnifOn (X)$
	fmucnd.2	$⊢ φ \to V \in UnifOn (Y)$
	fmucnd.3	$⊢ φ \to F \in (U uCn V)$
	fmucnd.4	$⊢ φ \to C \in CauFilU (U)$
	fmucnd.5	$⊢ D = ran (a \in C ⟼ F [a])$
Assertion	fmucnd	$⊢ φ \to D \in CauFilU (V)$

Proof

Step	Hyp	Ref	Expression
1		fmucnd.1	$⊢ φ \to U \in UnifOn (X)$
2		fmucnd.2	$⊢ φ \to V \in UnifOn (Y)$
3		fmucnd.3	$⊢ φ \to F \in (U uCn V)$
4		fmucnd.4	$⊢ φ \to C \in CauFilU (U)$
5		fmucnd.5	$⊢ D = ran (a \in C ⟼ F [a])$
6		cfilufbas	$⊢ (U \in UnifOn (X) \land C \in CauFilU (U)) \to C \in fBas (X)$
7	1 4 6	syl2anc	$⊢ φ \to C \in fBas (X)$
8		isucn	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall v \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) v F (y))))$
9	8	simprbda	$⊢ ((U \in UnifOn (X) \land V \in UnifOn (Y)) \land F \in (U uCn V)) \to F : X ⟶ Y$
10	1 2 3 9	syl21anc	$⊢ φ \to F : X ⟶ Y$
11	2	elfvexd	$⊢ φ \to Y \in V$
12	5	fbasrn	$⊢ (C \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to D \in fBas (Y)$
13	7 10 11 12	syl3anc	$⊢ φ \to D \in fBas (Y)$
14		simplr	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to a \in C$
15		eqid	$⊢ F [a] = F [a]$
16		imaeq2	$⊢ c = a \to F [c] = F [a]$
17	16	rspceeqv	$⊢ (a \in C \land F [a] = F [a]) \to \exists c \in C F [a] = F [c]$
18	14 15 17	sylancl	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to \exists c \in C F [a] = F [c]$
19		imaexg	$⊢ F \in (U uCn V) \to F [a] \in V$
20		eqid	$⊢ (c \in C ⟼ F [c]) = (c \in C ⟼ F [c])$
21	20	elrnmpt	$⊢ F [a] \in V \to (F [a] \in ran (c \in C ⟼ F [c]) \leftrightarrow \exists c \in C F [a] = F [c])$
22	3 19 21	3syl	$⊢ φ \to (F [a] \in ran (c \in C ⟼ F [c]) \leftrightarrow \exists c \in C F [a] = F [c])$
23	22	ad3antrrr	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to (F [a] \in ran (c \in C ⟼ F [c]) \leftrightarrow \exists c \in C F [a] = F [c])$
24	18 23	mpbird	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to F [a] \in ran (c \in C ⟼ F [c])$
25		imaeq2	$⊢ a = c \to F [a] = F [c]$
26	25	cbvmptv	$⊢ (a \in C ⟼ F [a]) = (c \in C ⟼ F [c])$
27	26	rneqi	$⊢ ran (a \in C ⟼ F [a]) = ran (c \in C ⟼ F [c])$
28	5 27	eqtri	$⊢ D = ran (c \in C ⟼ F [c])$
29	24 28	eleqtrrdi	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to F [a] \in D$
30	10	ffnd	$⊢ φ \to F Fn X$
31	30	ad3antrrr	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to F Fn X$
32		fbelss	$⊢ (C \in fBas (X) \land a \in C) \to a \subseteq X$
33	7 32	sylan	$⊢ (φ \land a \in C) \to a \subseteq X$
34	33	ad4ant13	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to a \subseteq X$
35		fmucndlem	$⊢ (F Fn X \land a \subseteq X) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [a \times a] = F [a] \times F [a]$
36	31 34 35	syl2anc	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [a \times a] = F [a] \times F [a]$
37		eqid	$⊢ (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) = (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)$
38	37	mpofun	$⊢ Fun (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)$
39		funimass2	$⊢ (Fun (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [a \times a] \subseteq v$
40	38 39	mpan	$⊢ a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v] \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [a \times a] \subseteq v$
41	40	adantl	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [a \times a] \subseteq v$
42	36 41	eqsstrrd	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to F [a] \times F [a] \subseteq v$
43		id	$⊢ b = F [a] \to b = F [a]$
44	43	sqxpeqd	$⊢ b = F [a] \to b \times b = F [a] \times F [a]$
45	44	sseq1d	$⊢ b = F [a] \to (b \times b \subseteq v \leftrightarrow F [a] \times F [a] \subseteq v)$
46	45	rspcev	$⊢ (F [a] \in D \land F [a] \times F [a] \subseteq v) \to \exists b \in D b \times b \subseteq v$
47	29 42 46	syl2anc	$⊢ (((φ \land v \in V) \land a \in C) \land a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]) \to \exists b \in D b \times b \subseteq v$
48	1	adantr	$⊢ (φ \land v \in V) \to U \in UnifOn (X)$
49	4	adantr	$⊢ (φ \land v \in V) \to C \in CauFilU (U)$
50	2	adantr	$⊢ (φ \land v \in V) \to V \in UnifOn (Y)$
51	3	adantr	$⊢ (φ \land v \in V) \to F \in (U uCn V)$
52		simpr	$⊢ (φ \land v \in V) \to v \in V$
53		nfcv	$⊢ \underline{Ⅎ} s ⟨F (x), F (y)⟩$
54		nfcv	$⊢ \underline{Ⅎ} t ⟨F (x), F (y)⟩$
55		nfcv	$⊢ \underline{Ⅎ} x ⟨F (s), F (t)⟩$
56		nfcv	$⊢ \underline{Ⅎ} y ⟨F (s), F (t)⟩$
57		simpl	$⊢ (x = s \land y = t) \to x = s$
58	57	fveq2d	$⊢ (x = s \land y = t) \to F (x) = F (s)$
59		simpr	$⊢ (x = s \land y = t) \to y = t$
60	59	fveq2d	$⊢ (x = s \land y = t) \to F (y) = F (t)$
61	58 60	opeq12d	$⊢ (x = s \land y = t) \to ⟨F (x), F (y)⟩ = ⟨F (s), F (t)⟩$
62	53 54 55 56 61	cbvmpo	$⊢ (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) = (s \in X, t \in X ⟼ ⟨F (s), F (t)⟩)$
63	48 50 51 52 62	ucnprima	$⊢ (φ \land v \in V) \to {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v] \in U$
64		cfiluexsm	$⊢ (U \in UnifOn (X) \land C \in CauFilU (U) \land {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v] \in U) \to \exists a \in C a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]$
65	48 49 63 64	syl3anc	$⊢ (φ \land v \in V) \to \exists a \in C a \times a \subseteq {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)}^{-1} [v]$
66	47 65	r19.29a	$⊢ (φ \land v \in V) \to \exists b \in D b \times b \subseteq v$
67	66	ralrimiva	$⊢ φ \to \forall v \in V \exists b \in D b \times b \subseteq v$
68		iscfilu	$⊢ V \in UnifOn (Y) \to (D \in CauFilU (V) \leftrightarrow (D \in fBas (Y) \land \forall v \in V \exists b \in D b \times b \subseteq v))$
69	2 68	syl	$⊢ φ \to (D \in CauFilU (V) \leftrightarrow (D \in fBas (Y) \land \forall v \in V \exists b \in D b \times b \subseteq v))$
70	13 67 69	mpbir2and	$⊢ φ \to D \in CauFilU (V)$

Metamath Proof Explorer

Theorem fmucnd

Proof