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 24309

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 2734	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2734	. . . . . . . 8 ⊢ (UnifSt‘𝑅) = (UnifSt‘𝑅)
5		ucncn.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝑅)
6	3, 4, 5	isusp 24285	. . . . . . 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 2734	. . . . . . . 8 ⊢ (Base‘𝑆) = (Base‘𝑆)
11		eqid 2734	. . . . . . . 8 ⊢ (UnifSt‘𝑆) = (UnifSt‘𝑆)
12		ucncn.k	. . . . . . . 8 ⊢ 𝐾 = (TopOpen‘𝑆)
13	10, 11, 12	isusp 24285	. . . . . . 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 24302	. . . . 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 6101	. . . . 5 ⊢ (^◡𝐹 “ 𝑎) ⊆ dom 𝐹
21	19	fdmd 6746	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = (Base‘𝑅))
22	21	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅))
23	20, 22	sseqtrid 4047	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
24		simplll 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑)
25		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆))
26	23	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
27		simplr 769	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (^◡𝐹 “ 𝑎))
28	26, 27	sseldd 3995	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅))
29	18	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
30	29	r19.21bi 3248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
31		r19.12 3311	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
33	32	r19.21bi 3248	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
34	24, 25, 28, 33	syl21anc 838	. . . . . . . 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 24235	. . . . . . . . . . . 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 769	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅))
44	28	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅))
45		ustimasn 24252	. . . . . . . . . . 11 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
46	42, 43, 44, 45	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
47		simpr 484	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
48		simplr 769	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅))
49		simpllr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
50	15	ad5antr 734	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
51		simpllr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆))
52		ustrel 24235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠)
53	50, 51, 52	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠)
54		elrelimasn 6105	. . . . . . . . . . . . . . . . . . 19 ⊢ (Rel 𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
56	55	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}))
57	49, 56	sseldd 3995	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
58	57	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
59		ffn 6736	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅))
60		elpreima 7077	. . . . . . . . . . . . . . . . 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 3143	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
66	65	adantr 480	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
67		r19.26 3108	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))))
68		pm3.33 765	. . . . . . . . . . . . 13 ⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
69	68	ralimi 3080	. . . . . . . . . . . 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 1225	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟)
73		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥}))
74		elrelimasn 6105	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦))
75	74	biimpa 476	. . . . . . . . . . . . . 14 ⊢ ((Rel 𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
76	72, 73, 75	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
77		breq2 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦))
78		eleq1w 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (^◡𝐹 “ 𝑎)))
79	77, 78	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎))))
80		simpl3 1192	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
81		simpl2r 1226	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
82	81, 73	sseldd 3995	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅))
83	79, 80, 82	rspcdva 3622	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
84	76, 83	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (^◡𝐹 “ 𝑎))
85	84	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
86	85	ssrdv 4000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
87	36, 41, 46, 71, 86	syl121anc 1374	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
88	87	ex 412	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
89	88	reximdva 3165	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
90	35, 89	mpd 15	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
91		sneq 4640	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)})
92	91	imaeq2d 6079	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)}))
93	92	sseq1d 4026	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
94	93	rexbidv 3176	. . . . . . 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 2840	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆)))
100		elutop 24257	. . . . . . . . . . . 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 7077	. . . . . . . . . . 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 3622	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
112	90, 111	r19.29a 3159	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
113	112	ralrimiva 3143	. . . 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 2824	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅))))
118		elutop 24257	. . . . . . 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 3143	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)
124		ucncn.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ TopSp)
125	3, 5	istps 22955	. . . 4 ⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑅)))
126	124, 125	sylib 218	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅)))
127		ucncn.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ TopSp)
128	10, 12	istps 22955	. . . 4 ⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝑆)))
129	127, 128	sylib 218	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆)))
130		iscn 23258	. . 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 1536 ∈ wcel 2105 ∀wral 3058 ∃wrex 3067 ⊆ wss 3962 {csn 4630 class class class wbr 5147 ^◡ccnv 5687 dom cdm 5688 “ cima 5691 Rel wrel 5693 Fn wfn 6557 ⟶wf 6558 ‘cfv 6562 (class class class)co 7430 Basecbs 17244 TopOpenctopn 17467 TopOnctopon 22931 TopSpctps 22953 Cn ccn 23247 UnifOncust 24223 unifTopcutop 24254 UnifStcuss 24277 UnifSpcusp 24278 Cn_ucucn 24299

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-fv 6570 df-ov 7433 df-oprab 7434 df-mpo 7435 df-map 8866 df-top 22915 df-topon 22932 df-topsp 22954 df-cn 23250 df-ust 24224 df-utop 24255 df-usp 24281 df-ucn 24300

This theorem is referenced by: (None)

W3C validator