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 22891

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 2798	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2798	. . . . . . . 8 ⊢ (UnifSt‘𝑅) = (UnifSt‘𝑅)
5		ucncn.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝑅)
6	3, 4, 5	isusp 22867	. . . . . . 7 ⊢ (𝑅 ∈ UnifSp ↔ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅))))
7	6	simplbi 501	. . . . . 6 ⊢ (𝑅 ∈ UnifSp → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
8	2, 7	syl 17	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
9		ucncn.2	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ UnifSp)
10		eqid 2798	. . . . . . . 8 ⊢ (Base‘𝑆) = (Base‘𝑆)
11		eqid 2798	. . . . . . . 8 ⊢ (UnifSt‘𝑆) = (UnifSt‘𝑆)
12		ucncn.k	. . . . . . . 8 ⊢ 𝐾 = (TopOpen‘𝑆)
13	10, 11, 12	isusp 22867	. . . . . . 7 ⊢ (𝑆 ∈ UnifSp ↔ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆))))
14	13	simplbi 501	. . . . . 6 ⊢ (𝑆 ∈ UnifSp → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
15	9, 14	syl 17	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
16		isucn 22884	. . . . 5 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
17	8, 15, 16	syl2anc 587	. . . 4 ⊢ (𝜑 → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
18	1, 17	mpbid 235	. . 3 ⊢ (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))
19	18	simpld 498	. 2 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆))
20		cnvimass 5916	. . . . 5 ⊢ (^◡𝐹 “ 𝑎) ⊆ dom 𝐹
21	19	fdmd 6497	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = (Base‘𝑅))
22	21	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅))
23	20, 22	sseqtrid 3967	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
24		simplll 774	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑)
25		simpr 488	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆))
26	23	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
27		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (^◡𝐹 “ 𝑎))
28	26, 27	sseldd 3916	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅))
29	18	simprd 499	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
30	29	r19.21bi 3173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
31		r19.12 3283	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
33	32	r19.21bi 3173	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
34	24, 25, 28, 33	syl21anc 836	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
35	34	adantr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
36	24	ad3antrrr 729	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑)
37	8	ad5antr 733	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
38		simpr 488	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅))
39		ustrel 22817	. . . . . . . . . . . 12 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
40	37, 38, 39	syl2anc 587	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
41	40	adantr 484	. . . . . . . . . 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 729	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅))
45		ustimasn 22834	. . . . . . . . . . 11 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
46	42, 43, 44, 45	syl3anc 1368	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
47		simpr 488	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
48		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅))
49		simpllr 775	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
50	15	ad5antr 733	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
51		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆))
52		ustrel 22817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠)
53	50, 51, 52	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠)
54		elrelimasn 5920	. . . . . . . . . . . . . . . . . . 19 ⊢ (Rel 𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
56	55	biimpar 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}))
57	49, 56	sseldd 3916	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
58	57	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
59		ffn 6487	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅))
60		elpreima 6805	. . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
64	63	ex 416	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
65	64	ralrimiva 3149	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
66	65	adantr 484	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
67		r19.26 3137	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))))
68		pm3.33 764	. . . . . . . . . . . . 13 ⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
69	68	ralimi 3128	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
70	67, 69	sylbir 238	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
71	47, 66, 70	syl2anc 587	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
72		simpl2l 1223	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟)
73		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥}))
74		elrelimasn 5920	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦))
75	74	biimpa 480	. . . . . . . . . . . . . 14 ⊢ ((Rel 𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
76	72, 73, 75	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
77		breq2 5034	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦))
78		eleq1w 2872	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (^◡𝐹 “ 𝑎)))
79	77, 78	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎))))
80		simpl3 1190	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
81		simpl2r 1224	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
82	81, 73	sseldd 3916	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅))
83	79, 80, 82	rspcdva 3573	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
84	76, 83	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (^◡𝐹 “ 𝑎))
85	84	ex 416	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
86	85	ssrdv 3921	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
87	36, 41, 46, 71, 86	syl121anc 1372	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
88	87	ex 416	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
89	88	reximdva 3233	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
90	35, 89	mpd 15	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
91		sneq 4535	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)})
92	91	imaeq2d 5896	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)}))
93	92	sseq1d 3946	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
94	93	rexbidv 3256	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
95		simpr 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾)
96	13	simprbi 500	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ UnifSp → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
97	9, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
98	97	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
99	95, 98	eleqtrd 2892	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆)))
100		elutop 22839	. . . . . . . . . . . 12 ⊢ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
101	15, 100	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
102	101	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
103	99, 102	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))
104	103	simprd 499	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
105	104	adantr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
106		elpreima 6805	. . . . . . . . . . 11 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
107	19, 59, 106	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
108	107	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
109	108	biimpa 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))
110	109	simprd 499	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎)
111	94, 105, 110	rspcdva 3573	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
112	90, 111	r19.29a 3248	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
113	112	ralrimiva 3149	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
114	6	simprbi 500	. . . . . . . 8 ⊢ (𝑅 ∈ UnifSp → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
115	2, 114	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
116	115	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
117	116	eleq2d 2875	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅))))
118		elutop 22839	. . . . . . 7 ⊢ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
119	8, 118	syl 17	. . . . . 6 ⊢ (𝜑 → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
120	119	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
121	117, 120	bitrd 282	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
122	23, 113, 121	mpbir2and 712	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
123	122	ralrimiva 3149	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)
124		ucncn.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ TopSp)
125	3, 5	istps 21539	. . . 4 ⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑅)))
126	124, 125	sylib 221	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅)))
127		ucncn.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ TopSp)
128	10, 12	istps 21539	. . . 4 ⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝑆)))
129	127, 128	sylib 221	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆)))
130		iscn 21840	. . 3 ⊢ ((𝐽 ∈ (TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
131	126, 129, 130	syl2anc 587	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
132	19, 123, 131	mpbir2and 712	1 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 ⊆ wss 3881 {csn 4525 class class class wbr 5030 ^◡ccnv 5518 dom cdm 5519 “ cima 5522 Rel wrel 5524 Fn wfn 6319 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 Basecbs 16475 TopOpenctopn 16687 TopOnctopon 21515 TopSpctps 21537 Cn ccn 21829 UnifOncust 22805 unifTopcutop 22836 UnifStcuss 22859 UnifSpcusp 22860 Cn_ucucn 22881

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-map 8391 df-top 21499 df-topon 21516 df-topsp 21538 df-cn 21832 df-ust 22806 df-utop 22837 df-usp 22863 df-ucn 22882

This theorem is referenced by: (None)

W3C validator