Metamath Proof Explorer

Theorem isucn2

Description: The predicate " F is a uniformly continuous function from uniform space U to uniform space V ", expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018)

Ref Expression
Hypotheses isucn2.u ⊢ 𝑈 = ( ( 𝑋 × 𝑋 ) filGen 𝑅 )
isucn2.v ⊢ 𝑉 = ( ( 𝑌 × 𝑌 ) filGen 𝑆 )
isucn2.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
isucn2.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
isucn2.3 ⊢ ( 𝜑 → 𝑅 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
isucn2.4 ⊢ ( 𝜑 → 𝑆 ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) )
Assertion isucn2 ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isucn2.u ⊢ 𝑈 = ( ( 𝑋 × 𝑋 ) filGen 𝑅 )
2 isucn2.v ⊢ 𝑉 = ( ( 𝑌 × 𝑌 ) filGen 𝑆 )
3 isucn2.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
4 isucn2.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
5 isucn2.3 ⊢ ( 𝜑 → 𝑅 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
6 isucn2.4 ⊢ ( 𝜑 → 𝑆 ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) )
7 isucn ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ) )
8 3 4 7 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ) )
9 breq ⊢ ( 𝑣 = 𝑠 → ( ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
10 9 imbi2d ⊢ ( 𝑣 = 𝑠 → ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
11 10 ralbidv ⊢ ( 𝑣 = 𝑠 → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
12 11 rexralbidv ⊢ ( 𝑣 = 𝑠 → ( ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
13 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑠 ∈ 𝑆 ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
14 ssfg ⊢ ( 𝑆 ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) → 𝑆 ⊆ ( ( 𝑌 × 𝑌 ) filGen 𝑆 ) )
15 6 14 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( ( 𝑌 × 𝑌 ) filGen 𝑆 ) )
16 15 2 sseqtrrdi ⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝑆 ⊆ 𝑉 )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑆 ⊆ 𝑉 )
19 18 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑉 )
20 12 13 19 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 )
22 21 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝑅 ) )
23 elfg ⊢ ( 𝑅 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑢 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝑅 ) ↔ ( 𝑢 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 ) ) )
24 5 23 syl ⊢ ( 𝜑 → ( 𝑢 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝑅 ) ↔ ( 𝑢 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 ) ) )
25 24 simplbda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝑅 ) ) → ∃ 𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 )
26 22 25 syldan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 )
27 ssbr ⊢ ( 𝑟 ⊆ 𝑢 → ( 𝑥 𝑟 𝑦 → 𝑥 𝑢 𝑦 ) )
28 27 imim1d ⊢ ( 𝑟 ⊆ 𝑢 → ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ 𝑟 ⊆ 𝑢 ) → ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
30 29 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ 𝑟 ⊆ 𝑢 ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
31 30 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ 𝑟 ⊆ 𝑢 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
32 ralim ⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
33 32 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
34 ralim ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
35 31 33 34 3syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ 𝑟 ⊆ 𝑢 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
36 35 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 ⊆ 𝑢 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ) )
37 36 reximdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 → ∃ 𝑟 ∈ 𝑅 ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ∃ 𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 → ∃ 𝑟 ∈ 𝑅 ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ) )
39 26 38 mpd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑟 ∈ 𝑅 ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
40 r19.37v ⊢ ( ∃ 𝑟 ∈ 𝑅 ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
42 41 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
43 42 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑠 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
44 20 43 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
45 44 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
46 ssfg ⊢ ( 𝑅 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → 𝑅 ⊆ ( ( 𝑋 × 𝑋 ) filGen 𝑅 ) )
47 5 46 syl ⊢ ( 𝜑 → 𝑅 ⊆ ( ( 𝑋 × 𝑋 ) filGen 𝑅 ) )
48 47 1 sseqtrrdi ⊢ ( 𝜑 → 𝑅 ⊆ 𝑈 )
49 ssrexv ⊢ ( 𝑅 ⊆ 𝑈 → ( ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
50 breq ⊢ ( 𝑟 = 𝑢 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑢 𝑦 ) )
51 50 imbi1d ⊢ ( 𝑟 = 𝑢 → ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
52 51 2ralbidv ⊢ ( 𝑟 = 𝑢 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
53 52 cbvrexvw ⊢ ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
54 49 53 syl6ib ⊢ ( 𝑅 ⊆ 𝑈 → ( ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
55 48 54 syl ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
56 55 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
58 nfv ⊢ Ⅎ 𝑠 ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 )
59 nfra1 ⊢ Ⅎ 𝑠 ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) )
60 58 59 nfan ⊢ Ⅎ 𝑠 ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
61 nfv ⊢ Ⅎ 𝑠 𝑣 ∈ 𝑉
62 60 61 nfan ⊢ Ⅎ 𝑠 ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 )
63 rspa ⊢ ( ( ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
64 63 ad5ant24 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) )
65 simp-4l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) )
66 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → 𝑠 ∈ 𝑆 )
67 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → 𝑠 ⊆ 𝑣 )
68 ssbr ⊢ ( 𝑠 ⊆ 𝑣 → ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
69 68 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
70 69 imim2d ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
71 70 ralimdv ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
72 71 ralimdv ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
73 72 reximdv ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
74 65 66 67 73 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ( ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
75 64 74 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑠 ⊆ 𝑣 ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
76 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑆 ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) )
77 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
78 77 2 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( ( 𝑌 × 𝑌 ) filGen 𝑆 ) )
79 elfg ⊢ ( 𝑆 ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) → ( 𝑣 ∈ ( ( 𝑌 × 𝑌 ) filGen 𝑆 ) ↔ ( 𝑣 ⊆ ( 𝑌 × 𝑌 ) ∧ ∃ 𝑠 ∈ 𝑆 𝑠 ⊆ 𝑣 ) ) )
80 79 simplbda ⊢ ( ( 𝑆 ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) ∧ 𝑣 ∈ ( ( 𝑌 × 𝑌 ) filGen 𝑆 ) ) → ∃ 𝑠 ∈ 𝑆 𝑠 ⊆ 𝑣 )
81 76 78 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ∃ 𝑠 ∈ 𝑆 𝑠 ⊆ 𝑣 )
82 62 75 81 r19.29af ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
83 82 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
84 83 ex ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑠 ∈ 𝑆 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
85 57 84 syld ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
86 85 imp ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
87 45 86 impbida ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) )
88 87 pm5.32da ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑢 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ) )
89 8 88 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑠 ( 𝐹 ‘ 𝑦 ) ) ) ) )