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 24492

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 2765	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2765	. . . . . . . 8 ⊢ (UnifSt‘𝑅) = (UnifSt‘𝑅)
5		ucncn.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝑅)
6	3, 4, 5	isusp 24469	. . . . . . 7 ⊢ (𝑅 ∈ UnifSp ↔ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅))))
7	6	simplbi 502	. . . . . 6 ⊢ (𝑅 ∈ UnifSp → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
8	2, 7	syl 18	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
9		ucncn.2	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ UnifSp)
10		eqid 2765	. . . . . . . 8 ⊢ (Base‘𝑆) = (Base‘𝑆)
11		eqid 2765	. . . . . . . 8 ⊢ (UnifSt‘𝑆) = (UnifSt‘𝑆)
12		ucncn.k	. . . . . . . 8 ⊢ 𝐾 = (TopOpen‘𝑆)
13	10, 11, 12	isusp 24469	. . . . . . 7 ⊢ (𝑆 ∈ UnifSp ↔ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆))))
14	13	simplbi 502	. . . . . 6 ⊢ (𝑆 ∈ UnifSp → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
15	9, 14	syl 18	. . . . 5 ⊢ (𝜑 → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
16		isucn 24485	. . . . 5 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cn_u(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))))
17	8, 15, 16	syl2anc 596	. . . 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 500	. 2 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆))
20		cnvimass 6086	. . . . 5 ⊢ (^◡𝐹 “ 𝑎) ⊆ dom 𝐹
21	19	fdmd 6720	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = (Base‘𝑅))
22	21	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅))
23	20, 22	sseqtrid 3980	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
24		simplll 787	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑)
25		simpr 490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆))
26	23	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅))
27		simplr 781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (^◡𝐹 “ 𝑎))
28	26, 27	sseldd 3939	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅))
29	18	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
30	29	r19.21bi 3259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
31		r19.12 3316	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
32	30, 31	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
33	32	r19.21bi 3259	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
34	24, 25, 28, 33	syl21anc 851	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
35	34	adantr 486	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
36	24	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑)
37	8	ad5antr 747	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
38		simpr 490	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅))
39		ustrel 24420	. . . . . . . . . . . 12 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
40	37, 38, 39	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
41	40	adantr 486	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → Rel 𝑟)
42	36, 8	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
43		simplr 781	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅))
44	28	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅))
45		ustimasn 24436	. . . . . . . . . . 11 ⊢ (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
46	42, 43, 44, 45	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
47		simpr 490	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
48		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅))
49		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
50	15	ad5antr 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
51		simpllr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆))
52		ustrel 24420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠)
53	50, 51, 52	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠)
54		elrelimasn 6090	. . . . . . . . . . . . . . . . . . 19 ⊢ (Rel 𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧)))
56	55	biimpar 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}))
57	49, 56	sseldd 3939	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
58	57	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎)
59		ffn 6709	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅))
60		elpreima 7057	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
61	19, 59, 60	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
62	61	ad7antr 751	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎)))
63	48, 58, 62	mpbir2and 726	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
64	63	ex 418	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
65	64	ralrimiva 3159	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
66	65	adantr 486	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
67		r19.26 3127	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))))
68		pm3.33 777	. . . . . . . . . . . . 13 ⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
69	68	ralimi 3104	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
70	67, 69	sylbir 238	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
71	47, 66, 70	syl2anc 596	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
72		simpl2l 1245	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟)
73		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥}))
74		elrelimasn 6090	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦))
75	74	biimpa 482	. . . . . . . . . . . . . 14 ⊢ ((Rel 𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
76	72, 73, 75	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
77		breq2 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦))
78		eleq1w 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (^◡𝐹 “ 𝑎)))
79	77, 78	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎))))
80		simpl3 1212	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎)))
81		simpl2r 1246	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
82	81, 73	sseldd 3939	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅))
83	79, 80, 82	rspcdva 3584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
84	76, 83	mpd 16	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (^◡𝐹 “ 𝑎))
85	84	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (^◡𝐹 “ 𝑎)))
86	85	ssrdv 3944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (^◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
87	36, 41, 46, 71, 86	syl121anc 1402	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
88	87	ex 418	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
89	88	reximdva 3180	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎)))
90	35, 89	mpd 16	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
91		sneq 4601	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)})
92	91	imaeq2d 6064	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)}))
93	92	sseq1d 3969	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
94	93	rexbidv 3191	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎))
95		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾)
96	13	simprbi 503	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ UnifSp → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
97	9, 96	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
98	97	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
99	95, 98	eleqtrd 2867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆)))
100		elutop 24441	. . . . . . . . . . . 12 ⊢ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
101	15, 100	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
102	101	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
103	99, 102	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))
104	103	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
105	104	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
106		elpreima 7057	. . . . . . . . . . 11 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
107	19, 59, 106	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
108	107	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)))
109	108	biimpa 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))
110	109	simprd 501	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎)
111	94, 105, 110	rspcdva 3584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)
112	90, 111	r19.29a 3175	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
113	112	ralrimiva 3159	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))
114	6	simprbi 503	. . . . . . . 8 ⊢ (𝑅 ∈ UnifSp → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
115	2, 114	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
116	115	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
117	116	eleq2d 2851	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅))))
118		elutop 24441	. . . . . . 7 ⊢ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
119	8, 118	syl 18	. . . . . 6 ⊢ (𝜑 → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
120	119	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
121	117, 120	bitrd 282	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((^◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((^◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (^◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (^◡𝐹 “ 𝑎))))
122	23, 113, 121	mpbir2and 726	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
123	122	ralrimiva 3159	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)
124		ucncn.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ TopSp)
125	3, 5	istps 23141	. . . 4 ⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑅)))
126	124, 125	sylib 221	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅)))
127		ucncn.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ TopSp)
128	10, 12	istps 23141	. . . 4 ⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝑆)))
129	127, 128	sylib 221	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆)))
130		iscn 23442	. . 3 ⊢ ((𝐽 ∈ (TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
131	126, 129, 130	syl2anc 596	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝐽)))
132	19, 123, 131	mpbir2and 726	1 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ∀wral 3081 ∃wrex 3091 ⊆ wss 3906 {csn 4591 class class class wbr 5111 ^◡ccnv 5662 dom cdm 5663 “ cima 5666 Rel wrel 5668 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 Basecbs 17291 TopOpenctopn 17496 TopOnctopon 23117 TopSpctps 23139 Cn ccn 23431 UnifOncust 24408 unifTopcutop 24438 UnifStcuss 24461 UnifSpcusp 24462 Cn_ucucn 24482

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-map 8832 df-top 23101 df-topon 23118 df-topsp 23140 df-cn 23434 df-ust 24409 df-utop 24439 df-usp 24465 df-ucn 24483

This theorem is used by: (None)

W3C validator