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

Theorem ucncn 24234
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‘𝑅) Cnu(UnifSt‘𝑆)))
Assertion
Ref Expression
ucncn (𝜑𝐹 ∈ (𝐽 Cn 𝐾))

Proof of Theorem ucncn
Dummy variables 𝑟 𝑎 𝑠 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ucncn.5 . . . 4 (𝜑𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)))
2 ucncn.1 . . . . . 6 (𝜑𝑅 ∈ UnifSp)
3 eqid 2725 . . . . . . . 8 (Base‘𝑅) = (Base‘𝑅)
4 eqid 2725 . . . . . . . 8 (UnifSt‘𝑅) = (UnifSt‘𝑅)
5 ucncn.j . . . . . . . 8 𝐽 = (TopOpen‘𝑅)
63, 4, 5isusp 24210 . . . . . . 7 (𝑅 ∈ UnifSp ↔ ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅))))
76simplbi 496 . . . . . 6 (𝑅 ∈ UnifSp → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
82, 7syl 17 . . . . 5 (𝜑 → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
9 ucncn.2 . . . . . 6 (𝜑𝑆 ∈ UnifSp)
10 eqid 2725 . . . . . . . 8 (Base‘𝑆) = (Base‘𝑆)
11 eqid 2725 . . . . . . . 8 (UnifSt‘𝑆) = (UnifSt‘𝑆)
12 ucncn.k . . . . . . . 8 𝐾 = (TopOpen‘𝑆)
1310, 11, 12isusp 24210 . . . . . . 7 (𝑆 ∈ UnifSp ↔ ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆))))
1413simplbi 496 . . . . . 6 (𝑆 ∈ UnifSp → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
159, 14syl 17 . . . . 5 (𝜑 → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
16 isucn 24227 . . . . 5 (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))))
178, 15, 16syl2anc 582 . . . 4 (𝜑 → (𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))))
181, 17mpbid 231 . . 3 (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))))
1918simpld 493 . 2 (𝜑𝐹:(Base‘𝑅)⟶(Base‘𝑆))
20 cnvimass 6086 . . . . 5 (𝐹𝑎) ⊆ dom 𝐹
2119fdmd 6733 . . . . . 6 (𝜑 → dom 𝐹 = (Base‘𝑅))
2221adantr 479 . . . . 5 ((𝜑𝑎𝐾) → dom 𝐹 = (Base‘𝑅))
2320, 22sseqtrid 4029 . . . 4 ((𝜑𝑎𝐾) → (𝐹𝑎) ⊆ (Base‘𝑅))
24 simplll 773 . . . . . . . . 9 ((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑)
25 simpr 483 . . . . . . . . 9 ((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆))
2623ad2antrr 724 . . . . . . . . . 10 ((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (𝐹𝑎) ⊆ (Base‘𝑅))
27 simplr 767 . . . . . . . . . 10 ((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (𝐹𝑎))
2826, 27sseldd 3977 . . . . . . . . 9 ((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅))
2918simprd 494 . . . . . . . . . . . 12 (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
3029r19.21bi 3238 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
31 r19.12 3301 . . . . . . . . . . 11 (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
3230, 31syl 17 . . . . . . . . . 10 ((𝜑𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
3332r19.21bi 3238 . . . . . . . . 9 (((𝜑𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
3424, 25, 28, 33syl21anc 836 . . . . . . . 8 ((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
3534adantr 479 . . . . . . 7 (((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
3624ad3antrrr 728 . . . . . . . . . 10 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → 𝜑)
378ad5antr 732 . . . . . . . . . . . 12 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
38 simpr 483 . . . . . . . . . . . 12 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅))
39 ustrel 24160 . . . . . . . . . . . 12 (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
4037, 38, 39syl2anc 582 . . . . . . . . . . 11 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟)
4140adantr 479 . . . . . . . . . 10 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → Rel 𝑟)
4236, 8syl 17 . . . . . . . . . . 11 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)))
43 simplr 767 . . . . . . . . . . 11 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → 𝑟 ∈ (UnifSt‘𝑅))
4428ad3antrrr 728 . . . . . . . . . . 11 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → 𝑥 ∈ (Base‘𝑅))
45 ustimasn 24177 . . . . . . . . . . 11 (((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
4642, 43, 44, 45syl3anc 1368 . . . . . . . . . 10 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
47 simpr 483 . . . . . . . . . . 11 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)))
48 simplr 767 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → 𝑧 ∈ (Base‘𝑅))
49 simpllr 774 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎)
5015ad5antr 732 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)))
51 simpllr 774 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆))
52 ustrel 24160 . . . . . . . . . . . . . . . . . . . 20 (((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠)
5350, 51, 52syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠)
54 elrelimasn 6090 . . . . . . . . . . . . . . . . . . 19 (Rel 𝑠 → ((𝐹𝑧) ∈ (𝑠 “ {(𝐹𝑥)}) ↔ (𝐹𝑥)𝑠(𝐹𝑧)))
5553, 54syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹𝑧) ∈ (𝑠 “ {(𝐹𝑥)}) ↔ (𝐹𝑥)𝑠(𝐹𝑧)))
5655biimpar 476 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → (𝐹𝑧) ∈ (𝑠 “ {(𝐹𝑥)}))
5749, 56sseldd 3977 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → (𝐹𝑧) ∈ 𝑎)
5857adantlr 713 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → (𝐹𝑧) ∈ 𝑎)
59 ffn 6723 . . . . . . . . . . . . . . . . 17 (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅))
60 elpreima 7066 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹𝑧) ∈ 𝑎)))
6119, 59, 603syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹𝑧) ∈ 𝑎)))
6261ad7antr 736 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹𝑧) ∈ 𝑎)))
6348, 58, 62mpbir2and 711 . . . . . . . . . . . . . 14 ((((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹𝑥)𝑠(𝐹𝑧)) → 𝑧 ∈ (𝐹𝑎))
6463ex 411 . . . . . . . . . . . . 13 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎)))
6564ralrimiva 3135 . . . . . . . . . . . 12 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎)))
6665adantr 479 . . . . . . . . . . 11 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎)))
67 r19.26 3100 . . . . . . . . . . . 12 (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) ∧ ((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎))))
68 pm3.33 763 . . . . . . . . . . . . 13 (((𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) ∧ ((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎))) → (𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎)))
6968ralimi 3072 . . . . . . . . . . . 12 (∀𝑧 ∈ (Base‘𝑅)((𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) ∧ ((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎)))
7067, 69sylbir 234 . . . . . . . . . . 11 ((∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹𝑥)𝑠(𝐹𝑧) → 𝑧 ∈ (𝐹𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎)))
7147, 66, 70syl2anc 582 . . . . . . . . . 10 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎)))
72 simpl2l 1223 . . . . . . . . . . . . . 14 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟)
73 simpr 483 . . . . . . . . . . . . . 14 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥}))
74 elrelimasn 6090 . . . . . . . . . . . . . . 15 (Rel 𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦))
7574biimpa 475 . . . . . . . . . . . . . 14 ((Rel 𝑟𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
7672, 73, 75syl2anc 582 . . . . . . . . . . . . 13 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦)
77 breq2 5153 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑥𝑟𝑧𝑥𝑟𝑦))
78 eleq1w 2808 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑧 ∈ (𝐹𝑎) ↔ 𝑦 ∈ (𝐹𝑎)))
7977, 78imbi12d 343 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎)) ↔ (𝑥𝑟𝑦𝑦 ∈ (𝐹𝑎))))
80 simpl3 1190 . . . . . . . . . . . . . 14 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎)))
81 simpl2r 1224 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅))
8281, 73sseldd 3977 . . . . . . . . . . . . . 14 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅))
8379, 80, 82rspcdva 3607 . . . . . . . . . . . . 13 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦𝑦 ∈ (𝐹𝑎)))
8476, 83mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝐹𝑎))
8584ex 411 . . . . . . . . . . 11 ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (𝐹𝑎)))
8685ssrdv 3982 . . . . . . . . . 10 ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧𝑧 ∈ (𝐹𝑎))) → (𝑟 “ {𝑥}) ⊆ (𝐹𝑎))
8736, 41, 46, 71, 86syl121anc 1372 . . . . . . . . 9 (((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧))) → (𝑟 “ {𝑥}) ⊆ (𝐹𝑎))
8887ex 411 . . . . . . . 8 ((((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) → (𝑟 “ {𝑥}) ⊆ (𝐹𝑎)))
8988reximdva 3157 . . . . . . 7 (((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹𝑥)𝑠(𝐹𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎)))
9035, 89mpd 15 . . . . . 6 (((((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))
91 sneq 4640 . . . . . . . . . 10 (𝑦 = (𝐹𝑥) → {𝑦} = {(𝐹𝑥)})
9291imaeq2d 6064 . . . . . . . . 9 (𝑦 = (𝐹𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹𝑥)}))
9392sseq1d 4008 . . . . . . . 8 (𝑦 = (𝐹𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎))
9493rexbidv 3168 . . . . . . 7 (𝑦 = (𝐹𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎))
95 simpr 483 . . . . . . . . . . 11 ((𝜑𝑎𝐾) → 𝑎𝐾)
9613simprbi 495 . . . . . . . . . . . . 13 (𝑆 ∈ UnifSp → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
979, 96syl 17 . . . . . . . . . . . 12 (𝜑𝐾 = (unifTop‘(UnifSt‘𝑆)))
9897adantr 479 . . . . . . . . . . 11 ((𝜑𝑎𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆)))
9995, 98eleqtrd 2827 . . . . . . . . . 10 ((𝜑𝑎𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆)))
100 elutop 24182 . . . . . . . . . . . 12 ((UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦𝑎𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
10115, 100syl 17 . . . . . . . . . . 11 (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦𝑎𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
102101adantr 479 . . . . . . . . . 10 ((𝜑𝑎𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦𝑎𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)))
10399, 102mpbid 231 . . . . . . . . 9 ((𝜑𝑎𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦𝑎𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))
104103simprd 494 . . . . . . . 8 ((𝜑𝑎𝐾) → ∀𝑦𝑎𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
105104adantr 479 . . . . . . 7 (((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) → ∀𝑦𝑎𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)
106 elpreima 7066 . . . . . . . . . . 11 (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (𝐹𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹𝑥) ∈ 𝑎)))
10719, 59, 1063syl 18 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝐹𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹𝑥) ∈ 𝑎)))
108107adantr 479 . . . . . . . . 9 ((𝜑𝑎𝐾) → (𝑥 ∈ (𝐹𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹𝑥) ∈ 𝑎)))
109108biimpa 475 . . . . . . . 8 (((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹𝑥) ∈ 𝑎))
110109simprd 494 . . . . . . 7 (((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) → (𝐹𝑥) ∈ 𝑎)
11194, 105, 110rspcdva 3607 . . . . . 6 (((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹𝑥)}) ⊆ 𝑎)
11290, 111r19.29a 3151 . . . . 5 (((𝜑𝑎𝐾) ∧ 𝑥 ∈ (𝐹𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))
113112ralrimiva 3135 . . . 4 ((𝜑𝑎𝐾) → ∀𝑥 ∈ (𝐹𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))
1146simprbi 495 . . . . . . . 8 (𝑅 ∈ UnifSp → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
1152, 114syl 17 . . . . . . 7 (𝜑𝐽 = (unifTop‘(UnifSt‘𝑅)))
116115adantr 479 . . . . . 6 ((𝜑𝑎𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅)))
117116eleq2d 2811 . . . . 5 ((𝜑𝑎𝐾) → ((𝐹𝑎) ∈ 𝐽 ↔ (𝐹𝑎) ∈ (unifTop‘(UnifSt‘𝑅))))
118 elutop 24182 . . . . . . 7 ((UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅)) → ((𝐹𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((𝐹𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (𝐹𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))))
1198, 118syl 17 . . . . . 6 (𝜑 → ((𝐹𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((𝐹𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (𝐹𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))))
120119adantr 479 . . . . 5 ((𝜑𝑎𝐾) → ((𝐹𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((𝐹𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (𝐹𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))))
121117, 120bitrd 278 . . . 4 ((𝜑𝑎𝐾) → ((𝐹𝑎) ∈ 𝐽 ↔ ((𝐹𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (𝐹𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (𝐹𝑎))))
12223, 113, 121mpbir2and 711 . . 3 ((𝜑𝑎𝐾) → (𝐹𝑎) ∈ 𝐽)
123122ralrimiva 3135 . 2 (𝜑 → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝐽)
124 ucncn.3 . . . 4 (𝜑𝑅 ∈ TopSp)
1253, 5istps 22880 . . . 4 (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑅)))
126124, 125sylib 217 . . 3 (𝜑𝐽 ∈ (TopOn‘(Base‘𝑅)))
127 ucncn.4 . . . 4 (𝜑𝑆 ∈ TopSp)
12810, 12istps 22880 . . . 4 (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝑆)))
129127, 128sylib 217 . . 3 (𝜑𝐾 ∈ (TopOn‘(Base‘𝑆)))
130 iscn 23183 . . 3 ((𝐽 ∈ (TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝐽)))
131126, 129, 130syl2anc 582 . 2 (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝐽)))
13219, 123, 131mpbir2and 711 1 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  wrex 3059  wss 3944  {csn 4630   class class class wbr 5149  ccnv 5677  dom cdm 5678  cima 5681  Rel wrel 5683   Fn wfn 6544  wf 6545  cfv 6549  (class class class)co 7419  Basecbs 17183  TopOpenctopn 17406  TopOnctopon 22856  TopSpctps 22878   Cn ccn 23172  UnifOncust 24148  unifTopcutop 24179  UnifStcuss 24202  UnifSpcusp 24203   Cnucucn 24224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-map 8847  df-top 22840  df-topon 22857  df-topsp 22879  df-cn 23175  df-ust 24149  df-utop 24180  df-usp 24206  df-ucn 24225
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator