ucncn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ucncn		Structured version Visualization version GIF version

Theorem ucncn 22417

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

**Hypotheses**
Ref	Expression
ucncn.j	⊢ 𝐽 = (TopOpen‘𝑅)
ucncn.k	⊢ 𝐾 = (TopOpen‘𝑆)
ucncn.1	⊢ (𝜑 → 𝑅 ∈ UnifSp)
ucncn.2	⊢ (𝜑 → 𝑆 ∈ UnifSp)
ucncn.3	⊢ (𝜑 → 𝑅 ∈ TopSp)
ucncn.4	⊢ (𝜑 → 𝑆 ∈ TopSp)
ucncn.5	⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)))

**Assertion**
Ref	Expression
ucncn	⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))

Proof of Theorem ucncn Dummy variables 𝑟 𝑎 𝑠 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ucncn.5	. . . 4 ⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)))
2		ucncn.1	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ UnifSp)
3		eqid 2799	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2799	. . . . . . . 8 ⊢ (UnifSt‘𝑅) = (UnifSt‘𝑅)
5		ucncn.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝑅)
6	3, 4, 5	isusp 22393	. . . . . . 7 ⊢ (𝑅 ∈ UnifSp ↔ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅))))
7	6	simplbi 492	. . . . . 6 ⊢ (𝑅 ∈ UnifSp → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
8	2, 7	syl 17	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
9		ucncn.2	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ UnifSp)
10		eqid 2799	. . . . . . . 8 ⊢ (Base‘𝑆) = (Base‘𝑆)
11		eqid 2799	. . . . . . . 8 ⊢ (UnifSt‘𝑆) = (UnifSt‘𝑆)
12		ucncn.k	. . . . . . . 8 ⊢ 𝐾 = (TopOpen‘𝑆)
13	10, 11, 12	isusp 22393	. . . . . . 7 ⊢ (𝑆 ∈ UnifSp ↔ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆))))
14	13	simplbi 492	. . . . . 6 ⊢ (𝑆 ∈ UnifSp → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
15	9, 14	syl 17	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
16		isucn 22410	. . . . 5 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
17	8, 15, 16	syl2anc 580	. . . 4 ⊢ (𝜑 → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
18	1, 17	mpbid 224	. . 3 ⊢ (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))
19	18	simpld 489	. 2 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆))
20		cnvimass 5702	. . . . 5 ⊢ (^◡𝐹 “ 𝑎) ⊆ dom 𝐹
21	19	fdmd 6265	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = (Base‘𝑅))
22	21	adantr 473	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅))
23	20, 22	syl5sseq 3849	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
24		simplll 792	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑)
25		simpr 478	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆))
26	23	ad2antrr 718	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
27		simplr 786	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (^◡𝐹 “ 𝑎))
28	26, 27	sseldd 3799	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅))
29	18	simprd 490	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
30	29	r19.21bi 3113	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
31		r19.12 3244	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
33	32	r19.21bi 3113	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
34	24, 25, 28, 33	syl21anc 867	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
35	34	adantr 473	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
36	24	ad3antrrr 722	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑)
37	8	ad5antr 729	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
38		simpr 478	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅))
39		ustrel 22343	. . . . . . . . . . . 12 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
40	37, 38, 39	syl2anc 580	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
41	40	adantr 473	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → Rel 𝑟)
42	36, 8	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
43		simplr 786	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅))
44	28	ad3antrrr 722	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅))
45		ustimasn 22360	. . . . . . . . . . 11 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
46	42, 43, 44, 45	syl3anc 1491	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
47		simpr 478	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
48		simplr 786	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅))
49		simpllr 794	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
50	15	ad5antr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
51		simpllr 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆))
52		ustrel 22343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠)
53	50, 51, 52	syl2anc 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠)
54		elrelimasn 5706	. . . . . . . . . . . . . . . . . . 19 ⊢ (Rel 𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
56	55	biimpar 470	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}))
57	49, 56	sseldd 3799	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
58	57	adantlr 707	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
59		ffn 6256	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅))
60		elpreima 6563	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
61	19, 59, 60	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
62	61	ad7antr 737	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
63	48, 58, 62	mpbir2and 705	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
64	63	ex 402	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
65	64	ralrimiva 3147	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
66	65	adantr 473	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
67		r19.26 3245	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))))
68		pm3.33 782	. . . . . . . . . . . . 13 ⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
69	68	ralimi 3133	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
70	67, 69	sylbir 227	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
71	47, 66, 70	syl2anc 580	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
72		simpl2l 1298	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟)
73		simpr 478	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥}))
74		elrelimasn 5706	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦))
75	74	biimpa 469	. . . . . . . . . . . . . 14 ⊢ ((Rel 𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
76	72, 73, 75	syl2anc 580	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
77		breq2 4847	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦))
78		eleq1w 2861	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (^◡𝐹 “ 𝑎)))
79	77, 78	imbi12d 336	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎))))
80		simpl3 1247	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
81		simpl2r 1300	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
82	81, 73	sseldd 3799	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅))
83	79, 80, 82	rspcdva 3503	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
84	76, 83	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (^◡𝐹 “ 𝑎))
85	84	ex 402	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
86	85	ssrdv 3804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
87	36, 41, 46, 71, 86	syl121anc 1495	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
88	87	ex 402	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
89	88	reximdva 3197	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
90	35, 89	mpd 15	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
91		sneq 4378	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)})
92	91	imaeq2d 5683	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)}))
93	92	sseq1d 3828	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
94	93	rexbidv 3233	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
95		simpr 478	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾)
96	13	simprbi 491	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ UnifSp → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
97	9, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
98	97	adantr 473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
99	95, 98	eleqtrd 2880	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆)))
100		elutop 22365	. . . . . . . . . . . 12 ⊢ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
101	15, 100	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
102	101	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
103	99, 102	mpbid 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))
104	103	simprd 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
105	104	adantr 473	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
106		elpreima 6563	. . . . . . . . . . 11 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
107	19, 59, 106	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
108	107	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
109	108	biimpa 469	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))
110	109	simprd 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎)
111	94, 105, 110	rspcdva 3503	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
112	90, 111	r19.29a 3259	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
113	112	ralrimiva 3147	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
114	6	simprbi 491	. . . . . . . 8 ⊢ (𝑅 ∈ UnifSp → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
115	2, 114	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
116	115	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
117	116	eleq2d 2864	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅))))
118		elutop 22365	. . . . . . 7 ⊢ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
119	8, 118	syl 17	. . . . . 6 ⊢ (𝜑 → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
120	119	adantr 473	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
121	117, 120	bitrd 271	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
122	23, 113, 121	mpbir2and 705	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
123	122	ralrimiva 3147	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)
124		ucncn.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ TopSp)
125	3, 5	istps 21067	. . . 4 ⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑅)))
126	124, 125	sylib 210	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅)))
127		ucncn.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ TopSp)
128	10, 12	istps 21067	. . . 4 ⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝑆)))
129	127, 128	sylib 210	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆)))
130		iscn 21368	. . 3 ⊢ ((𝐽 ∈ (TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
131	126, 129, 130	syl2anc 580	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
132	19, 123, 131	mpbir2and 705	1 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ∀wral 3089 ∃wrex 3090 ⊆ wss 3769 {csn 4368 class class class wbr 4843 ^◡ccnv 5311 dom cdm 5312 “ cima 5315 Rel wrel 5317 Fn wfn 6096 ⟶wf 6097 ‘cfv 6101 (class class class)co 6878 Basecbs 16184 TopOpenctopn 16397 TopOnctopon 21043 TopSpctps 21065 Cn ccn 21357 UnifOncust 22331 unifTopcutop 22362 UnifStcuss 22385 UnifSpcusp 22386 Cn_ucucn 22407

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-fv 6109 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-map 8097 df-top 21027 df-topon 21044 df-topsp 21066 df-cn 21360 df-ust 22332 df-utop 22363 df-usp 22389 df-ucn 22408

This theorem is referenced by: (None)

W3C validator