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 ‘ 𝑅 ) Cn_u ( 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 ‘ 𝑅 ) Cn_u ( 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 ‘ 𝑅 ) Cn_u ( UnifSt ‘ 𝑆 ) ) ↔ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑠 ∈ ( UnifSt ‘ 𝑆 ) ∃ 𝑟 ∈ ( UnifSt ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑥 𝑟 𝑧 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑧 ) ) ) ) )
19	12 17 18	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( UnifSt ‘ 𝑅 ) Cn_u ( 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 𝐾 ) )

Metamath Proof Explorer

Theorem ucncn

Proof