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

Theorem isucn2 23766
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 23765 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
41, 2, 3syl2anc 585 . 2 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
5 breq 5149 . . . . . . . . . 10 (𝑣 = 𝑠 → ((𝐹𝑥)𝑣(𝐹𝑦) ↔ (𝐹𝑥)𝑠(𝐹𝑦)))
65imbi2d 341 . . . . . . . . 9 (𝑣 = 𝑠 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
76ralbidv 3178 . . . . . . . 8 (𝑣 = 𝑠 → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
87rexralbidv 3221 . . . . . . 7 (𝑣 = 𝑠 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
9 simplr 768 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
10 isucn2.4 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
11 ssfg 23358 . . . . . . . . . . . 12 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
1210, 11syl 17 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
13 isucn2.v . . . . . . . . . . 11 𝑉 = ((𝑌 × 𝑌)filGen𝑆)
1412, 13sseqtrrdi 4032 . . . . . . . . . 10 (𝜑𝑆𝑉)
1514adantr 482 . . . . . . . . 9 ((𝜑𝐹:𝑋𝑌) → 𝑆𝑉)
1615adantr 482 . . . . . . . 8 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → 𝑆𝑉)
1716sselda 3981 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → 𝑠𝑉)
188, 9, 17rspcdva 3613 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
19 simpr 486 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → 𝑢𝑈)
20 isucn2.u . . . . . . . . . . . 12 𝑈 = ((𝑋 × 𝑋)filGen𝑅)
2119, 20eleqtrdi 2844 . . . . . . . . . . 11 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅))
22 isucn2.3 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ (fBas‘(𝑋 × 𝑋)))
23 elfg 23357 . . . . . . . . . . . . 13 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2422, 23syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2524simplbda 501 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) → ∃𝑟𝑅 𝑟𝑢)
2621, 25syldan 592 . . . . . . . . . 10 ((𝜑𝑢𝑈) → ∃𝑟𝑅 𝑟𝑢)
27 ssbr 5191 . . . . . . . . . . . . . . . . . 18 (𝑟𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
2827imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑟𝑢 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
2928adantl 483 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3029ralrimivw 3151 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3130ralrimivw 3151 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
32 ralim 3087 . . . . . . . . . . . . . . 15 (∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3332ralimi 3084 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
34 ralim 3087 . . . . . . . . . . . . . 14 (∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3531, 33, 343syl 18 . . . . . . . . . . . . 13 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3635ex 414 . . . . . . . . . . . 12 ((𝜑𝑟𝑅) → (𝑟𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3736reximdva 3169 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3837adantr 482 . . . . . . . . . 10 ((𝜑𝑢𝑈) → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3926, 38mpd 15 . . . . . . . . 9 ((𝜑𝑢𝑈) → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
40 r19.37v 3182 . . . . . . . . 9 (∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4139, 40syl 17 . . . . . . . 8 ((𝜑𝑢𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4241rexlimdva 3156 . . . . . . 7 (𝜑 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4342ad3antrrr 729 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4418, 43mpd 15 . . . . 5 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
4544ralrimiva 3147 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
46 ssfg 23358 . . . . . . . . . . 11 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4722, 46syl 17 . . . . . . . . . 10 (𝜑𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4847, 20sseqtrrdi 4032 . . . . . . . . 9 (𝜑𝑅𝑈)
49 ssrexv 4050 . . . . . . . . . 10 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
50 breq 5149 . . . . . . . . . . . . 13 (𝑟 = 𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
5150imbi1d 342 . . . . . . . . . . . 12 (𝑟 = 𝑢 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
52512ralbidv 3219 . . . . . . . . . . 11 (𝑟 = 𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5352cbvrexvw 3236 . . . . . . . . . 10 (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
5449, 53syl6ib 251 . . . . . . . . 9 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5548, 54syl 17 . . . . . . . 8 (𝜑 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5655ralimdv 3170 . . . . . . 7 (𝜑 → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5756adantr 482 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
58 nfv 1918 . . . . . . . . . . 11 𝑠(𝜑𝐹:𝑋𝑌)
59 nfra1 3282 . . . . . . . . . . 11 𝑠𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))
6058, 59nfan 1903 . . . . . . . . . 10 𝑠((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
61 nfv 1918 . . . . . . . . . 10 𝑠 𝑣𝑉
6260, 61nfan 1903 . . . . . . . . 9 𝑠(((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉)
63 rspa 3246 . . . . . . . . . . 11 ((∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
6463ad5ant24 760 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
65 simp-4l 782 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (𝜑𝐹:𝑋𝑌))
66 simplr 768 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑆)
67 simpr 486 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑣)
68 ssbr 5191 . . . . . . . . . . . . . . . 16 (𝑠𝑣 → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
6968adantl 483 . . . . . . . . . . . . . . 15 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7069imim2d 57 . . . . . . . . . . . . . 14 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7170ralimdv 3170 . . . . . . . . . . . . 13 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7271ralimdv 3170 . . . . . . . . . . . 12 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7372reximdv 3171 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7465, 66, 67, 73syl21anc 837 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7564, 74mpd 15 . . . . . . . . 9 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
7610ad3antrrr 729 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
77 simpr 486 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣𝑉)
7877, 13eleqtrdi 2844 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆))
79 elfg 23357 . . . . . . . . . . 11 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → (𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆) ↔ (𝑣 ⊆ (𝑌 × 𝑌) ∧ ∃𝑠𝑆 𝑠𝑣)))
8079simplbda 501 . . . . . . . . . 10 ((𝑆 ∈ (fBas‘(𝑌 × 𝑌)) ∧ 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) → ∃𝑠𝑆 𝑠𝑣)
8176, 78, 80syl2anc 585 . . . . . . . . 9 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑠𝑆 𝑠𝑣)
8262, 75, 81r19.29af 3266 . . . . . . . 8 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8382ralrimiva 3147 . . . . . . 7 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8483ex 414 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8557, 84syld 47 . . . . 5 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8685imp 408 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8745, 86impbida 800 . . 3 ((𝜑𝐹:𝑋𝑌) → (∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
8887pm5.32da 580 . 2 (𝜑 → ((𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
894, 88bitrd 279 1 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  wrex 3071  wss 3947   class class class wbr 5147   × cxp 5673  wf 6536  cfv 6540  (class class class)co 7404  fBascfbas 20917  filGencfg 20918  UnifOncust 23686   Cnucucn 23762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-map 8818  df-fbas 20926  df-fg 20927  df-ust 23687  df-ucn 23763
This theorem is referenced by:  metucn  24062
  Copyright terms: Public domain W3C validator