Metamath Proof Explorer

Theorem ucncn

Description: Uniform continuity implies continuity. Deduction form. Proposition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Hypotheses ucncn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
ucncn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑆 )
ucncn.1 ⊢ ( 𝜑 → 𝑅 ∈ UnifSp )
ucncn.2 ⊢ ( 𝜑 → 𝑆 ∈ UnifSp )
ucncn.3 ⊢ ( 𝜑 → 𝑅 ∈ TopSp )
ucncn.4 ⊢ ( 𝜑 → 𝑆 ∈ TopSp )
ucncn.5 ⊢ ( 𝜑 → 𝐹 ∈ ( ( UnifSt ‘ 𝑅 ) Cnu ( UnifSt ‘ 𝑆 ) ) )
Assertion ucncn ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ucncn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
2 ucncn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑆 )
3 ucncn.1 ⊢ ( 𝜑 → 𝑅 ∈ UnifSp )
4 ucncn.2 ⊢ ( 𝜑 → 𝑆 ∈ UnifSp )
5 ucncn.3 ⊢ ( 𝜑 → 𝑅 ∈ TopSp )
6 ucncn.4 ⊢ ( 𝜑 → 𝑆 ∈ TopSp )
7 ucncn.5 ⊢ ( 𝜑 → 𝐹 ∈ ( ( UnifSt ‘ 𝑅 ) Cnu ( UnifSt ‘ 𝑆 ) ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( UnifSt ‘ 𝑅 ) = ( UnifSt ‘ 𝑅 )
10 8 9 1 isusp ⊢ ( 𝑅 ∈ UnifSp ↔ ( ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) ∧ 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) ) )
11 10 simplbi ⊢ ( 𝑅 ∈ UnifSp → ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) )
12 3 11 syl ⊢ ( 𝜑 → ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) )
13 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14 eqid ⊢ ( UnifSt ‘ 𝑆 ) = ( UnifSt ‘ 𝑆 )
15 13 14 2 isusp ⊢ ( 𝑆 ∈ UnifSp ↔ ( ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) ∧ 𝐾 = ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) ) )
16 15 simplbi ⊢ ( 𝑆 ∈ UnifSp → ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) )
17 4 16 syl ⊢ ( 𝜑 → ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) )
18 isucn ⊢ ( ( ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) ∧ ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ∈ ( ( UnifSt ‘ 𝑅 ) Cnu ( UnifSt ‘ 𝑆 ) ) ↔ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) ) )
19 12 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( UnifSt ‘ 𝑅 ) Cnu ( UnifSt ‘ 𝑆 ) ) ↔ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) ) )
20 7 19 mpbid ⊢ ( 𝜑 → ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) )
21 20 simpld ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
22 cnvimass ⊢ ( ◡ 𝐹 “ 𝑎 ) ⊆ dom 𝐹
23 21 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( Base ‘ 𝑅 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → dom 𝐹 = ( Base ‘ 𝑅 ) )
25 22 24 sseqtrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑎 ) ⊆ ( Base ‘ 𝑅 ) )
26 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → 𝜑 )
27 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → 𝑠 ∈ ( UnifSt ‘ 𝑆 ) )
28 25 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝑎 ) ⊆ ( Base ‘ 𝑅 ) )
29 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) )
30 28 29 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
31 20 simprd ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
32 31 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
33 r19.12 ⊢ ( ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
35 34 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
36 26 27 30 35 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
37 36 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
38 26 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → 𝜑 )
39 12 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) )
40 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → 𝑟 ∈ ( UnifSt ‘ 𝑅 ) )
41 ustrel ⊢ ( ( ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → Rel 𝑟 )
42 39 40 41 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → Rel 𝑟 )
43 42 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → Rel 𝑟 )
44 38 12 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) )
45 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → 𝑟 ∈ ( UnifSt ‘ 𝑅 ) )
46 30 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
47 ustimasn ⊢ ( ( ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) )
48 44 45 46 47 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) )
49 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
50 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
51 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 )
52 17 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) )
53 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → 𝑠 ∈ ( UnifSt ‘ 𝑆 ) )
54 ustrel ⊢ ( ( ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) → Rel 𝑠 )
55 52 53 54 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → Rel 𝑠 )
56 elrelimasn ⊢ ( Rel 𝑠 → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
57 55 56 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) )
58 57 biimpar ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) )
59 51 58 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑎 )
60 59 adantlr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑎 )
61 ffn ⊢ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
62 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑎 ) ) )
63 21 61 62 3syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑎 ) ) )
64 63 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑎 ) ) )
65 50 60 64 mpbir2and ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) )
66 65 ex ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
67 66 ralrimiva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
68 67 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
69 r19.26 ⊢ ( ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ↔ ( ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) )
70 pm3.33 ⊢ ( ( ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) → ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
71 70 ralimi ⊢ ( ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
72 69 71 sylbir ⊢ ( ( ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
73 49 68 72 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
74 simpl2l ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → Rel 𝑟 )
75 simpr ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) )
76 elrelimasn ⊢ ( Rel 𝑟 → ( 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ↔ 𝑥 𝑟 𝑦 ) )
77 76 biimpa ⊢ ( ( Rel 𝑟 ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → 𝑥 𝑟 𝑦 )
78 74 75 77 syl2anc ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → 𝑥 𝑟 𝑦 )
79 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 𝑟 𝑧 ↔ 𝑥 𝑟 𝑦 ) )
80 eleq1w ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
81 79 80 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ↔ ( 𝑥 𝑟 𝑦 → 𝑦 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) )
82 simpl3 ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
83 simpl2r ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) )
84 83 75 sseldd ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
85 81 82 84 rspcdva ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → ( 𝑥 𝑟 𝑦 → 𝑦 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
86 78 85 mpd ⊢ ( ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) ∧ 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑎 ) )
87 86 ex ⊢ ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) → ( 𝑦 ∈ ( 𝑟 “ { 𝑥 } ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑎 ) ) )
88 87 ssrdv ⊢ ( ( 𝜑 ∧ ( Rel 𝑟 ∧ ( 𝑟 “ { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → 𝑧 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ) → ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) )
89 38 43 48 73 88 syl121anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) )
90 89 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) ∧ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) ) )
91 90 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) → ( ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) ) )
92 37 91 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) ∧ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ) ∧ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) )
93 sneq ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → { 𝑦 } = { ( 𝐹 ‘ 𝑥 ) } )
94 93 imaeq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑠 “ { 𝑦 } ) = ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) )
95 94 sseq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 ↔ ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) )
96 95 rexbidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 ↔ ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 ) )
97 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → 𝑎 ∈ 𝐾 )
98 15 simprbi ⊢ ( 𝑆 ∈ UnifSp → 𝐾 = ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) )
99 4 98 syl ⊢ ( 𝜑 → 𝐾 = ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → 𝐾 = ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) )
101 97 100 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → 𝑎 ∈ ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) )
102 elutop ⊢ ( ( UnifSt ‘ 𝑆 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑆 ) ) → ( 𝑎 ∈ ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) ↔ ( 𝑎 ⊆ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑎 ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 ) ) )
103 17 102 syl ⊢ ( 𝜑 → ( 𝑎 ∈ ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) ↔ ( 𝑎 ⊆ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑎 ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( 𝑎 ∈ ( unifTop ‘ ( UnifSt ‘ 𝑆 ) ) ↔ ( 𝑎 ⊆ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑎 ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 ) ) )
105 101 104 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( 𝑎 ⊆ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑎 ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 ) )
106 105 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ∀ 𝑦 ∈ 𝑎 ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) → ∀ 𝑦 ∈ 𝑎 ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { 𝑦 } ) ⊆ 𝑎 )
108 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑎 ) ) )
109 21 61 108 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑎 ) ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑎 ) ) )
111 110 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑎 ) )
112 111 simprd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑎 )
113 96 107 112 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) → ∃ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ( 𝑠 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑎 )
114 92 113 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ) → ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) )
115 114 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) )
116 10 simprbi ⊢ ( 𝑅 ∈ UnifSp → 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) )
117 3 116 syl ⊢ ( 𝜑 → 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) )
119 118 eleq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑎 ) ∈ ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) ) )
120 elutop ⊢ ( ( UnifSt ‘ 𝑅 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑅 ) ) → ( ( ◡ 𝐹 “ 𝑎 ) ∈ ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) ↔ ( ( ◡ 𝐹 “ 𝑎 ) ⊆ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) ) ) )
121 12 120 syl ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑎 ) ∈ ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) ↔ ( ( ◡ 𝐹 “ 𝑎 ) ⊆ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) ) ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑎 ) ∈ ( unifTop ‘ ( UnifSt ‘ 𝑅 ) ) ↔ ( ( ◡ 𝐹 “ 𝑎 ) ⊆ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) ) ) )
123 119 122 bitrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝐽 ↔ ( ( ◡ 𝐹 “ 𝑎 ) ⊆ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑎 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ( 𝑟 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ 𝑎 ) ) ) )
124 25 115 123 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑎 ) ∈ 𝐽 )
125 124 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝐽 )
126 8 1 istps ⊢ ( 𝑅 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
127 5 126 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
128 13 2 istps ⊢ ( 𝑆 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
129 6 128 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
130 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝐽 ) ) )
131 127 129 130 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝐽 ) ) )
132 21 125 131 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )