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

Theorem isucn2 22304
 Description: The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉." , expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.)
Hypotheses
Ref Expression
isucn2.u 𝑈 = ((𝑋 × 𝑋)filGen𝑅)
isucn2.v 𝑉 = ((𝑌 × 𝑌)filGen𝑆)
isucn2.1 (𝜑𝑈 ∈ (UnifOn‘𝑋))
isucn2.2 (𝜑𝑉 ∈ (UnifOn‘𝑌))
isucn2.3 (𝜑𝑅 ∈ (fBas‘(𝑋 × 𝑋)))
isucn2.4 (𝜑𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
Assertion
Ref Expression
isucn2 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
Distinct variable groups:   𝑠,𝑟,𝑥,𝑦,𝐹   𝑅,𝑟,𝑥,𝑦   𝑆,𝑠,𝑥,𝑦   𝑈,𝑟,𝑠,𝑥,𝑦   𝑉,𝑠,𝑥   𝑋,𝑟,𝑠,𝑥,𝑦   𝑌,𝑠,𝑥,𝑦   𝜑,𝑟,𝑠,𝑥,𝑦
Allowed substitution hints:   𝑅(𝑠)   𝑆(𝑟)   𝑉(𝑦,𝑟)   𝑌(𝑟)

Proof of Theorem isucn2
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isucn2.1 . . 3 (𝜑𝑈 ∈ (UnifOn‘𝑋))
2 isucn2.2 . . 3 (𝜑𝑉 ∈ (UnifOn‘𝑌))
3 isucn 22303 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
41, 2, 3syl2anc 696 . 2 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
5 breq 4806 . . . . . . . . . 10 (𝑣 = 𝑠 → ((𝐹𝑥)𝑣(𝐹𝑦) ↔ (𝐹𝑥)𝑠(𝐹𝑦)))
65imbi2d 329 . . . . . . . . 9 (𝑣 = 𝑠 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
76ralbidv 3124 . . . . . . . 8 (𝑣 = 𝑠 → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
87rexralbidv 3196 . . . . . . 7 (𝑣 = 𝑠 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
9 simplr 809 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
10 isucn2.4 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
11 ssfg 21897 . . . . . . . . . . . 12 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
1210, 11syl 17 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
13 isucn2.v . . . . . . . . . . 11 𝑉 = ((𝑌 × 𝑌)filGen𝑆)
1412, 13syl6sseqr 3793 . . . . . . . . . 10 (𝜑𝑆𝑉)
1514adantr 472 . . . . . . . . 9 ((𝜑𝐹:𝑋𝑌) → 𝑆𝑉)
1615adantr 472 . . . . . . . 8 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → 𝑆𝑉)
1716sselda 3744 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → 𝑠𝑉)
188, 9, 17rspcdva 3455 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
19 simpr 479 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → 𝑢𝑈)
20 isucn2.u . . . . . . . . . . . 12 𝑈 = ((𝑋 × 𝑋)filGen𝑅)
2119, 20syl6eleq 2849 . . . . . . . . . . 11 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅))
22 isucn2.3 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ (fBas‘(𝑋 × 𝑋)))
23 elfg 21896 . . . . . . . . . . . . 13 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2422, 23syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2524simplbda 655 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) → ∃𝑟𝑅 𝑟𝑢)
2621, 25syldan 488 . . . . . . . . . 10 ((𝜑𝑢𝑈) → ∃𝑟𝑅 𝑟𝑢)
27 ssbr 4848 . . . . . . . . . . . . . . . . . 18 (𝑟𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
2827imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑟𝑢 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
2928adantl 473 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3029ralrimivw 3105 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3130ralrimivw 3105 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
32 ralim 3086 . . . . . . . . . . . . . . 15 (∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3332ralimi 3090 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
34 ralim 3086 . . . . . . . . . . . . . 14 (∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3531, 33, 343syl 18 . . . . . . . . . . . . 13 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3635ex 449 . . . . . . . . . . . 12 ((𝜑𝑟𝑅) → (𝑟𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3736reximdva 3155 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3837adantr 472 . . . . . . . . . 10 ((𝜑𝑢𝑈) → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3926, 38mpd 15 . . . . . . . . 9 ((𝜑𝑢𝑈) → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
40 r19.37v 3225 . . . . . . . . 9 (∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4139, 40syl 17 . . . . . . . 8 ((𝜑𝑢𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4241rexlimdva 3169 . . . . . . 7 (𝜑 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4342ad3antrrr 768 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4418, 43mpd 15 . . . . 5 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
4544ralrimiva 3104 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
46 ssfg 21897 . . . . . . . . . . 11 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4722, 46syl 17 . . . . . . . . . 10 (𝜑𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4847, 20syl6sseqr 3793 . . . . . . . . 9 (𝜑𝑅𝑈)
49 ssrexv 3808 . . . . . . . . . 10 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
50 breq 4806 . . . . . . . . . . . . 13 (𝑟 = 𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
5150imbi1d 330 . . . . . . . . . . . 12 (𝑟 = 𝑢 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
52512ralbidv 3127 . . . . . . . . . . 11 (𝑟 = 𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5352cbvrexv 3311 . . . . . . . . . 10 (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
5449, 53syl6ib 241 . . . . . . . . 9 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5548, 54syl 17 . . . . . . . 8 (𝜑 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5655ralimdv 3101 . . . . . . 7 (𝜑 → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5756adantr 472 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
58 nfv 1992 . . . . . . . . . . 11 𝑠(𝜑𝐹:𝑋𝑌)
59 nfra1 3079 . . . . . . . . . . 11 𝑠𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))
6058, 59nfan 1977 . . . . . . . . . 10 𝑠((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
61 nfv 1992 . . . . . . . . . 10 𝑠 𝑣𝑉
6260, 61nfan 1977 . . . . . . . . 9 𝑠(((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉)
63 simp-4r 827 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
64 simplr 809 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑆)
65 rspa 3068 . . . . . . . . . . 11 ((∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
6663, 64, 65syl2anc 696 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
67 simp-4l 825 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (𝜑𝐹:𝑋𝑌))
68 simpr 479 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑣)
69 ssbr 4848 . . . . . . . . . . . . . . . 16 (𝑠𝑣 → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7069adantl 473 . . . . . . . . . . . . . . 15 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7170imim2d 57 . . . . . . . . . . . . . 14 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7271ralimdv 3101 . . . . . . . . . . . . 13 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7372ralimdv 3101 . . . . . . . . . . . 12 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7473reximdv 3154 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7567, 64, 68, 74syl21anc 1476 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7666, 75mpd 15 . . . . . . . . 9 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
7710ad3antrrr 768 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
78 simpr 479 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣𝑉)
7978, 13syl6eleq 2849 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆))
80 elfg 21896 . . . . . . . . . . 11 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → (𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆) ↔ (𝑣 ⊆ (𝑌 × 𝑌) ∧ ∃𝑠𝑆 𝑠𝑣)))
8180simplbda 655 . . . . . . . . . 10 ((𝑆 ∈ (fBas‘(𝑌 × 𝑌)) ∧ 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) → ∃𝑠𝑆 𝑠𝑣)
8277, 79, 81syl2anc 696 . . . . . . . . 9 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑠𝑆 𝑠𝑣)
8362, 76, 82r19.29af 3214 . . . . . . . 8 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8483ralrimiva 3104 . . . . . . 7 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8584ex 449 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8657, 85syld 47 . . . . 5 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8786imp 444 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8845, 87impbida 913 . . 3 ((𝜑𝐹:𝑋𝑌) → (∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
8988pm5.32da 676 . 2 (𝜑 → ((𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
904, 89bitrd 268 1 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∀wral 3050  ∃wrex 3051   ⊆ wss 3715   class class class wbr 4804   × cxp 5264  ⟶wf 6045  ‘cfv 6049  (class class class)co 6814  fBascfbas 19956  filGencfg 19957  UnifOncust 22224   Cnucucn 22300 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-map 8027  df-fbas 19965  df-fg 19966  df-ust 22225  df-ucn 22301 This theorem is referenced by:  metucn  22597
 Copyright terms: Public domain W3C validator