ucncn

Description: Uniform continuity implies continuity. Deduction form. Proposition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017)

	Ref	Expression
Hypotheses	ucncn.j	$⊢ J = TopOpen (R)$
	ucncn.k	$⊢ K = TopOpen (S)$
	ucncn.1	$⊢ φ \to R \in UnifSp$
	ucncn.2	$⊢ φ \to S \in UnifSp$
	ucncn.3	$⊢ φ \to R \in TopSp$
	ucncn.4	$⊢ φ \to S \in TopSp$
	ucncn.5	$⊢ φ \to F \in (UnifSt (R) uCn UnifSt (S))$
Assertion	ucncn	$⊢ φ \to F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ucncn.j	$⊢ J = TopOpen (R)$
2		ucncn.k	$⊢ K = TopOpen (S)$
3		ucncn.1	$⊢ φ \to R \in UnifSp$
4		ucncn.2	$⊢ φ \to S \in UnifSp$
5		ucncn.3	$⊢ φ \to R \in TopSp$
6		ucncn.4	$⊢ φ \to S \in TopSp$
7		ucncn.5	$⊢ φ \to F \in (UnifSt (R) uCn UnifSt (S))$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ UnifSt (R) = UnifSt (R)$
10	8 9 1	isusp	$⊢ R \in UnifSp \leftrightarrow (UnifSt (R) \in UnifOn ({Base}_{R}) \land J = unifTop (UnifSt (R)))$
11	10	simplbi	$⊢ R \in UnifSp \to UnifSt (R) \in UnifOn ({Base}_{R})$
12	3 11	syl	$⊢ φ \to UnifSt (R) \in UnifOn ({Base}_{R})$
13		eqid	$⊢ {Base}_{S} = {Base}_{S}$
14		eqid	$⊢ UnifSt (S) = UnifSt (S)$
15	13 14 2	isusp	$⊢ S \in UnifSp \leftrightarrow (UnifSt (S) \in UnifOn ({Base}_{S}) \land K = unifTop (UnifSt (S)))$
16	15	simplbi	$⊢ S \in UnifSp \to UnifSt (S) \in UnifOn ({Base}_{S})$
17	4 16	syl	$⊢ φ \to UnifSt (S) \in UnifOn ({Base}_{S})$
18		isucn	$⊢ (UnifSt (R) \in UnifOn ({Base}_{R}) \land UnifSt (S) \in UnifOn ({Base}_{S})) \to (F \in (UnifSt (R) uCn UnifSt (S)) \leftrightarrow (F : {Base}_{R} ⟶ {Base}_{S} \land \forall s \in UnifSt (S) \exists r \in UnifSt (R) \forall x \in {Base}_{R} \forall z \in {Base}_{R} (x r z \to F (x) s F (z))))$
19	12 17 18	syl2anc	$⊢ φ \to (F \in (UnifSt (R) uCn UnifSt (S)) \leftrightarrow (F : {Base}_{R} ⟶ {Base}_{S} \land \forall s \in UnifSt (S) \exists r \in UnifSt (R) \forall x \in {Base}_{R} \forall z \in {Base}_{R} (x r z \to F (x) s F (z))))$
20	7 19	mpbid	$⊢ φ \to (F : {Base}_{R} ⟶ {Base}_{S} \land \forall s \in UnifSt (S) \exists r \in UnifSt (R) \forall x \in {Base}_{R} \forall z \in {Base}_{R} (x r z \to F (x) s F (z)))$
21	20	simpld	$⊢ φ \to F : {Base}_{R} ⟶ {Base}_{S}$
22		cnvimass	$⊢ F^{-1} [a] \subseteq dom F$
23	21	fdmd	$⊢ φ \to dom F = {Base}_{R}$
24	23	adantr	$⊢ (φ \land a \in K) \to dom F = {Base}_{R}$
25	22 24	sseqtrid	$⊢ (φ \land a \in K) \to F^{-1} [a] \subseteq {Base}_{R}$
26		simplll	$⊢ (((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \to φ$
27		simpr	$⊢ (((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \to s \in UnifSt (S)$
28	25	ad2antrr	$⊢ (((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \to F^{-1} [a] \subseteq {Base}_{R}$
29		simplr	$⊢ (((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \to x \in F^{-1} [a]$
30	28 29	sseldd	$⊢ (((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \to x \in {Base}_{R}$
31	20	simprd	$⊢ φ \to \forall s \in UnifSt (S) \exists r \in UnifSt (R) \forall x \in {Base}_{R} \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
32	31	r19.21bi	$⊢ (φ \land s \in UnifSt (S)) \to \exists r \in UnifSt (R) \forall x \in {Base}_{R} \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
33		r19.12	$⊢ \exists r \in UnifSt (R) \forall x \in {Base}_{R} \forall z \in {Base}_{R} (x r z \to F (x) s F (z)) \to \forall x \in {Base}_{R} \exists r \in UnifSt (R) \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
34	32 33	syl	$⊢ (φ \land s \in UnifSt (S)) \to \forall x \in {Base}_{R} \exists r \in UnifSt (R) \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
35	34	r19.21bi	$⊢ ((φ \land s \in UnifSt (S)) \land x \in {Base}_{R}) \to \exists r \in UnifSt (R) \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
36	26 27 30 35	syl21anc	$⊢ (((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \to \exists r \in UnifSt (R) \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
37	36	adantr	$⊢ ((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \to \exists r \in UnifSt (R) \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
38	26	ad3antrrr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to φ$
39	12	ad5antr	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to UnifSt (R) \in UnifOn ({Base}_{R})$
40		simpr	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to r \in UnifSt (R)$
41		ustrel	$⊢ (UnifSt (R) \in UnifOn ({Base}_{R}) \land r \in UnifSt (R)) \to Rel r$
42	39 40 41	syl2anc	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to Rel r$
43	42	adantr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to Rel r$
44	38 12	syl	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to UnifSt (R) \in UnifOn ({Base}_{R})$
45		simplr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to r \in UnifSt (R)$
46	30	ad3antrrr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to x \in {Base}_{R}$
47		ustimasn	$⊢ (UnifSt (R) \in UnifOn ({Base}_{R}) \land r \in UnifSt (R) \land x \in {Base}_{R}) \to r [\{x\}] \subseteq {Base}_{R}$
48	44 45 46 47	syl3anc	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to r [\{x\}] \subseteq {Base}_{R}$
49		simpr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to \forall z \in {Base}_{R} (x r z \to F (x) s F (z))$
50		simplr	$⊢ (((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land z \in {Base}_{R}) \land F (x) s F (z)) \to z \in {Base}_{R}$
51		simpllr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land F (x) s F (z)) \to s [\{F (x)\}] \subseteq a$
52	17	ad5antr	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to UnifSt (S) \in UnifOn ({Base}_{S})$
53		simpllr	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to s \in UnifSt (S)$
54		ustrel	$⊢ (UnifSt (S) \in UnifOn ({Base}_{S}) \land s \in UnifSt (S)) \to Rel s$
55	52 53 54	syl2anc	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to Rel s$
56		elrelimasn	$⊢ Rel s \to (F (z) \in s [\{F (x)\}] \leftrightarrow F (x) s F (z))$
57	55 56	syl	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to (F (z) \in s [\{F (x)\}] \leftrightarrow F (x) s F (z))$
58	57	biimpar	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land F (x) s F (z)) \to F (z) \in s [\{F (x)\}]$
59	51 58	sseldd	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land F (x) s F (z)) \to F (z) \in a$
60	59	adantlr	$⊢ (((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land z \in {Base}_{R}) \land F (x) s F (z)) \to F (z) \in a$
61		ffn	$⊢ F : {Base}_{R} ⟶ {Base}_{S} \to F Fn {Base}_{R}$
62		elpreima	$⊢ F Fn {Base}_{R} \to (z \in F^{-1} [a] \leftrightarrow (z \in {Base}_{R} \land F (z) \in a))$
63	21 61 62	3syl	$⊢ φ \to (z \in F^{-1} [a] \leftrightarrow (z \in {Base}_{R} \land F (z) \in a))$
64	63	ad7antr	$⊢ (((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land z \in {Base}_{R}) \land F (x) s F (z)) \to (z \in F^{-1} [a] \leftrightarrow (z \in {Base}_{R} \land F (z) \in a))$
65	50 60 64	mpbir2and	$⊢ (((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land z \in {Base}_{R}) \land F (x) s F (z)) \to z \in F^{-1} [a]$
66	65	ex	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land z \in {Base}_{R}) \to (F (x) s F (z) \to z \in F^{-1} [a])$
67	66	ralrimiva	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to \forall z \in {Base}_{R} (F (x) s F (z) \to z \in F^{-1} [a])$
68	67	adantr	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to \forall z \in {Base}_{R} (F (x) s F (z) \to z \in F^{-1} [a])$
69		r19.26	$⊢ \forall z \in {Base}_{R} ((x r z \to F (x) s F (z)) \land (F (x) s F (z) \to z \in F^{-1} [a])) \leftrightarrow (\forall z \in {Base}_{R} (x r z \to F (x) s F (z)) \land \forall z \in {Base}_{R} (F (x) s F (z) \to z \in F^{-1} [a]))$
70		pm3.33	$⊢ ((x r z \to F (x) s F (z)) \land (F (x) s F (z) \to z \in F^{-1} [a])) \to (x r z \to z \in F^{-1} [a])$
71	70	ralimi	$⊢ \forall z \in {Base}_{R} ((x r z \to F (x) s F (z)) \land (F (x) s F (z) \to z \in F^{-1} [a])) \to \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])$
72	69 71	sylbir	$⊢ (\forall z \in {Base}_{R} (x r z \to F (x) s F (z)) \land \forall z \in {Base}_{R} (F (x) s F (z) \to z \in F^{-1} [a])) \to \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])$
73	49 68 72	syl2anc	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])$
74		simpl2l	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to Rel r$
75		simpr	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to y \in r [\{x\}]$
76		elrelimasn	$⊢ Rel r \to (y \in r [\{x\}] \leftrightarrow x r y)$
77	76	biimpa	$⊢ (Rel r \land y \in r [\{x\}]) \to x r y$
78	74 75 77	syl2anc	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to x r y$
79		breq2	$⊢ z = y \to (x r z \leftrightarrow x r y)$
80		eleq1w	$⊢ z = y \to (z \in F^{-1} [a] \leftrightarrow y \in F^{-1} [a])$
81	79 80	imbi12d	$⊢ z = y \to ((x r z \to z \in F^{-1} [a]) \leftrightarrow (x r y \to y \in F^{-1} [a]))$
82		simpl3	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])$
83		simpl2r	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to r [\{x\}] \subseteq {Base}_{R}$
84	83 75	sseldd	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to y \in {Base}_{R}$
85	81 82 84	rspcdva	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to (x r y \to y \in F^{-1} [a])$
86	78 85	mpd	$⊢ ((φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \land y \in r [\{x\}]) \to y \in F^{-1} [a]$
87	86	ex	$⊢ (φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \to (y \in r [\{x\}] \to y \in F^{-1} [a])$
88	87	ssrdv	$⊢ (φ \land (Rel r \land r [\{x\}] \subseteq {Base}_{R}) \land \forall z \in {Base}_{R} (x r z \to z \in F^{-1} [a])) \to r [\{x\}] \subseteq F^{-1} [a]$
89	38 43 48 73 88	syl121anc	$⊢ ((((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \land \forall z \in {Base}_{R} (x r z \to F (x) s F (z))) \to r [\{x\}] \subseteq F^{-1} [a]$
90	89	ex	$⊢ (((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \land r \in UnifSt (R)) \to (\forall z \in {Base}_{R} (x r z \to F (x) s F (z)) \to r [\{x\}] \subseteq F^{-1} [a])$
91	90	reximdva	$⊢ ((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \to (\exists r \in UnifSt (R) \forall z \in {Base}_{R} (x r z \to F (x) s F (z)) \to \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a])$
92	37 91	mpd	$⊢ ((((φ \land a \in K) \land x \in F^{-1} [a]) \land s \in UnifSt (S)) \land s [\{F (x)\}] \subseteq a) \to \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]$
93		sneq	$⊢ y = F (x) \to \{y\} = \{F (x)\}$
94	93	imaeq2d	$⊢ y = F (x) \to s [\{y\}] = s [\{F (x)\}]$
95	94	sseq1d	$⊢ y = F (x) \to (s [\{y\}] \subseteq a \leftrightarrow s [\{F (x)\}] \subseteq a)$
96	95	rexbidv	$⊢ y = F (x) \to (\exists s \in UnifSt (S) s [\{y\}] \subseteq a \leftrightarrow \exists s \in UnifSt (S) s [\{F (x)\}] \subseteq a)$
97		simpr	$⊢ (φ \land a \in K) \to a \in K$
98	15	simprbi	$⊢ S \in UnifSp \to K = unifTop (UnifSt (S))$
99	4 98	syl	$⊢ φ \to K = unifTop (UnifSt (S))$
100	99	adantr	$⊢ (φ \land a \in K) \to K = unifTop (UnifSt (S))$
101	97 100	eleqtrd	$⊢ (φ \land a \in K) \to a \in unifTop (UnifSt (S))$
102		elutop	$⊢ UnifSt (S) \in UnifOn ({Base}_{S}) \to (a \in unifTop (UnifSt (S)) \leftrightarrow (a \subseteq {Base}_{S} \land \forall y \in a \exists s \in UnifSt (S) s [\{y\}] \subseteq a))$
103	17 102	syl	$⊢ φ \to (a \in unifTop (UnifSt (S)) \leftrightarrow (a \subseteq {Base}_{S} \land \forall y \in a \exists s \in UnifSt (S) s [\{y\}] \subseteq a))$
104	103	adantr	$⊢ (φ \land a \in K) \to (a \in unifTop (UnifSt (S)) \leftrightarrow (a \subseteq {Base}_{S} \land \forall y \in a \exists s \in UnifSt (S) s [\{y\}] \subseteq a))$
105	101 104	mpbid	$⊢ (φ \land a \in K) \to (a \subseteq {Base}_{S} \land \forall y \in a \exists s \in UnifSt (S) s [\{y\}] \subseteq a)$
106	105	simprd	$⊢ (φ \land a \in K) \to \forall y \in a \exists s \in UnifSt (S) s [\{y\}] \subseteq a$
107	106	adantr	$⊢ ((φ \land a \in K) \land x \in F^{-1} [a]) \to \forall y \in a \exists s \in UnifSt (S) s [\{y\}] \subseteq a$
108		elpreima	$⊢ F Fn {Base}_{R} \to (x \in F^{-1} [a] \leftrightarrow (x \in {Base}_{R} \land F (x) \in a))$
109	21 61 108	3syl	$⊢ φ \to (x \in F^{-1} [a] \leftrightarrow (x \in {Base}_{R} \land F (x) \in a))$
110	109	adantr	$⊢ (φ \land a \in K) \to (x \in F^{-1} [a] \leftrightarrow (x \in {Base}_{R} \land F (x) \in a))$
111	110	biimpa	$⊢ ((φ \land a \in K) \land x \in F^{-1} [a]) \to (x \in {Base}_{R} \land F (x) \in a)$
112	111	simprd	$⊢ ((φ \land a \in K) \land x \in F^{-1} [a]) \to F (x) \in a$
113	96 107 112	rspcdva	$⊢ ((φ \land a \in K) \land x \in F^{-1} [a]) \to \exists s \in UnifSt (S) s [\{F (x)\}] \subseteq a$
114	92 113	r19.29a	$⊢ ((φ \land a \in K) \land x \in F^{-1} [a]) \to \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]$
115	114	ralrimiva	$⊢ (φ \land a \in K) \to \forall x \in F^{-1} [a] \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]$
116	10	simprbi	$⊢ R \in UnifSp \to J = unifTop (UnifSt (R))$
117	3 116	syl	$⊢ φ \to J = unifTop (UnifSt (R))$
118	117	adantr	$⊢ (φ \land a \in K) \to J = unifTop (UnifSt (R))$
119	118	eleq2d	$⊢ (φ \land a \in K) \to (F^{-1} [a] \in J \leftrightarrow F^{-1} [a] \in unifTop (UnifSt (R)))$
120		elutop	$⊢ UnifSt (R) \in UnifOn ({Base}_{R}) \to (F^{-1} [a] \in unifTop (UnifSt (R)) \leftrightarrow (F^{-1} [a] \subseteq {Base}_{R} \land \forall x \in F^{-1} [a] \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]))$
121	12 120	syl	$⊢ φ \to (F^{-1} [a] \in unifTop (UnifSt (R)) \leftrightarrow (F^{-1} [a] \subseteq {Base}_{R} \land \forall x \in F^{-1} [a] \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]))$
122	121	adantr	$⊢ (φ \land a \in K) \to (F^{-1} [a] \in unifTop (UnifSt (R)) \leftrightarrow (F^{-1} [a] \subseteq {Base}_{R} \land \forall x \in F^{-1} [a] \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]))$
123	119 122	bitrd	$⊢ (φ \land a \in K) \to (F^{-1} [a] \in J \leftrightarrow (F^{-1} [a] \subseteq {Base}_{R} \land \forall x \in F^{-1} [a] \exists r \in UnifSt (R) r [\{x\}] \subseteq F^{-1} [a]))$
124	25 115 123	mpbir2and	$⊢ (φ \land a \in K) \to F^{-1} [a] \in J$
125	124	ralrimiva	$⊢ φ \to \forall a \in K F^{-1} [a] \in J$
126	8 1	istps	$⊢ R \in TopSp \leftrightarrow J \in TopOn ({Base}_{R})$
127	5 126	sylib	$⊢ φ \to J \in TopOn ({Base}_{R})$
128	13 2	istps	$⊢ S \in TopSp \leftrightarrow K \in TopOn ({Base}_{S})$
129	6 128	sylib	$⊢ φ \to K \in TopOn ({Base}_{S})$
130		iscn	$⊢ (J \in TopOn ({Base}_{R}) \land K \in TopOn ({Base}_{S})) \to (F \in (J Cn K) \leftrightarrow (F : {Base}_{R} ⟶ {Base}_{S} \land \forall a \in K F^{-1} [a] \in J))$
131	127 129 130	syl2anc	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : {Base}_{R} ⟶ {Base}_{S} \land \forall a \in K F^{-1} [a] \in J))$
132	21 125 131	mpbir2and	$⊢ φ \to F \in (J Cn K)$

Metamath Proof Explorer

Theorem ucncn

Proof