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 24170

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 2729	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2729	. . . . . . . 8 ⊢ (UnifSt‘𝑅) = (UnifSt‘𝑅)
5		ucncn.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝑅)
6	3, 4, 5	isusp 24147	. . . . . . 7 ⊢ (𝑅 ∈ UnifSp ↔ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅))))
7	6	simplbi 497	. . . . . 6 ⊢ (𝑅 ∈ UnifSp → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
8	2, 7	syl 17	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
9		ucncn.2	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ UnifSp)
10		eqid 2729	. . . . . . . 8 ⊢ (Base‘𝑆) = (Base‘𝑆)
11		eqid 2729	. . . . . . . 8 ⊢ (UnifSt‘𝑆) = (UnifSt‘𝑆)
12		ucncn.k	. . . . . . . 8 ⊢ 𝐾 = (TopOpen‘𝑆)
13	10, 11, 12	isusp 24147	. . . . . . 7 ⊢ (𝑆 ∈ UnifSp ↔ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆))))
14	13	simplbi 497	. . . . . 6 ⊢ (𝑆 ∈ UnifSp → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
15	9, 14	syl 17	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
16		isucn 24163	. . . . 5 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
17	8, 15, 16	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
18	1, 17	mpbid 232	. . 3 ⊢ (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))
19	18	simpld 494	. 2 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆))
20		cnvimass 6033	. . . . 5 ⊢ (^◡𝐹 “ 𝑎) ⊆ dom 𝐹
21	19	fdmd 6662	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = (Base‘𝑅))
22	21	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅))
23	20, 22	sseqtrid 3978	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
24		simplll 774	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑)
25		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆))
26	23	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
27		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (^◡𝐹 “ 𝑎))
28	26, 27	sseldd 3936	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅))
29	18	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
30	29	r19.21bi 3221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
31		r19.12 3278	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
33	32	r19.21bi 3221	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
34	24, 25, 28, 33	syl21anc 837	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
35	34	adantr 480	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
36	24	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑)
37	8	ad5antr 734	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
38		simpr 484	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅))
39		ustrel 24097	. . . . . . . . . . . 12 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
40	37, 38, 39	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
41	40	adantr 480	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → Rel 𝑟)
42	36, 8	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
43		simplr 768	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅))
44	28	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅))
45		ustimasn 24114	. . . . . . . . . . 11 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
46	42, 43, 44, 45	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
47		simpr 484	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
48		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅))
49		simpllr 775	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
50	15	ad5antr 734	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
51		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆))
52		ustrel 24097	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠)
53	50, 51, 52	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠)
54		elrelimasn 6037	. . . . . . . . . . . . . . . . . . 19 ⊢ (Rel 𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
56	55	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}))
57	49, 56	sseldd 3936	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
58	57	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
59		ffn 6652	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅))
60		elpreima 6992	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
61	19, 59, 60	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
62	61	ad7antr 738	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
63	48, 58, 62	mpbir2and 713	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
64	63	ex 412	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
65	64	ralrimiva 3121	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
66	65	adantr 480	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
67		r19.26 3089	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))))
68		pm3.33 764	. . . . . . . . . . . . 13 ⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
69	68	ralimi 3066	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
70	67, 69	sylbir 235	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
71	47, 66, 70	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
72		simpl2l 1227	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟)
73		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥}))
74		elrelimasn 6037	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦))
75	74	biimpa 476	. . . . . . . . . . . . . 14 ⊢ ((Rel 𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
76	72, 73, 75	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
77		breq2 5096	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦))
78		eleq1w 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (^◡𝐹 “ 𝑎)))
79	77, 78	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎))))
80		simpl3 1194	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
81		simpl2r 1228	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
82	81, 73	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅))
83	79, 80, 82	rspcdva 3578	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
84	76, 83	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (^◡𝐹 “ 𝑎))
85	84	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
86	85	ssrdv 3941	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
87	36, 41, 46, 71, 86	syl121anc 1377	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
88	87	ex 412	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
89	88	reximdva 3142	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
90	35, 89	mpd 15	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
91		sneq 4587	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)})
92	91	imaeq2d 6011	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)}))
93	92	sseq1d 3967	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
94	93	rexbidv 3153	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
95		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾)
96	13	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ UnifSp → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
97	9, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
98	97	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
99	95, 98	eleqtrd 2830	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆)))
100		elutop 24119	. . . . . . . . . . . 12 ⊢ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
101	15, 100	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
102	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
103	99, 102	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))
104	103	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
105	104	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
106		elpreima 6992	. . . . . . . . . . 11 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
107	19, 59, 106	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
108	107	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
109	108	biimpa 476	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))
110	109	simprd 495	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎)
111	94, 105, 110	rspcdva 3578	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
112	90, 111	r19.29a 3137	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
113	112	ralrimiva 3121	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
114	6	simprbi 496	. . . . . . . 8 ⊢ (𝑅 ∈ UnifSp → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
115	2, 114	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
116	115	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
117	116	eleq2d 2814	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅))))
118		elutop 24119	. . . . . . 7 ⊢ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
119	8, 118	syl 17	. . . . . 6 ⊢ (𝜑 → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
120	119	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
121	117, 120	bitrd 279	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
122	23, 113, 121	mpbir2and 713	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
123	122	ralrimiva 3121	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)
124		ucncn.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ TopSp)
125	3, 5	istps 22819	. . . 4 ⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑅)))
126	124, 125	sylib 218	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅)))
127		ucncn.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ TopSp)
128	10, 12	istps 22819	. . . 4 ⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝑆)))
129	127, 128	sylib 218	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆)))
130		iscn 23120	. . 3 ⊢ ((𝐽 ∈ (TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
131	126, 129, 130	syl2anc 584	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
132	19, 123, 131	mpbir2and 713	1 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 ⊆ wss 3903 {csn 4577 class class class wbr 5092 ^◡ccnv 5618 dom cdm 5619 “ cima 5622 Rel wrel 5624 Fn wfn 6477 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 Basecbs 17120 TopOpenctopn 17325 TopOnctopon 22795 TopSpctps 22817 Cn ccn 23109 UnifOncust 24085 unifTopcutop 24116 UnifStcuss 24139 UnifSpcusp 24140 Cn_ucucn 24160

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-br 5093 df-opab 5155 df-mpt 5174 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-fv 6490 df-ov 7352 df-oprab 7353 df-mpo 7354 df-map 8755 df-top 22779 df-topon 22796 df-topsp 22818 df-cn 23112 df-ust 24086 df-utop 24117 df-usp 24143 df-ucn 24161

This theorem is referenced by: (None)

W3C validator