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

Theorem isucn2 22454
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 22453 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
41, 2, 3syl2anc 581 . 2 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
5 breq 4876 . . . . . . . . . 10 (𝑣 = 𝑠 → ((𝐹𝑥)𝑣(𝐹𝑦) ↔ (𝐹𝑥)𝑠(𝐹𝑦)))
65imbi2d 332 . . . . . . . . 9 (𝑣 = 𝑠 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
76ralbidv 3196 . . . . . . . 8 (𝑣 = 𝑠 → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
87rexralbidv 3269 . . . . . . 7 (𝑣 = 𝑠 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
9 simplr 787 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
10 isucn2.4 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
11 ssfg 22047 . . . . . . . . . . . 12 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
1210, 11syl 17 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
13 isucn2.v . . . . . . . . . . 11 𝑉 = ((𝑌 × 𝑌)filGen𝑆)
1412, 13syl6sseqr 3878 . . . . . . . . . 10 (𝜑𝑆𝑉)
1514adantr 474 . . . . . . . . 9 ((𝜑𝐹:𝑋𝑌) → 𝑆𝑉)
1615adantr 474 . . . . . . . 8 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → 𝑆𝑉)
1716sselda 3828 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → 𝑠𝑉)
188, 9, 17rspcdva 3533 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
19 simpr 479 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → 𝑢𝑈)
20 isucn2.u . . . . . . . . . . . 12 𝑈 = ((𝑋 × 𝑋)filGen𝑅)
2119, 20syl6eleq 2917 . . . . . . . . . . 11 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅))
22 isucn2.3 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ (fBas‘(𝑋 × 𝑋)))
23 elfg 22046 . . . . . . . . . . . . 13 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2422, 23syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2524simplbda 495 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) → ∃𝑟𝑅 𝑟𝑢)
2621, 25syldan 587 . . . . . . . . . 10 ((𝜑𝑢𝑈) → ∃𝑟𝑅 𝑟𝑢)
27 ssbr 4918 . . . . . . . . . . . . . . . . . 18 (𝑟𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
2827imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑟𝑢 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
2928adantl 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3029ralrimivw 3177 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3130ralrimivw 3177 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
32 ralim 3158 . . . . . . . . . . . . . . 15 (∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3332ralimi 3162 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
34 ralim 3158 . . . . . . . . . . . . . 14 (∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3531, 33, 343syl 18 . . . . . . . . . . . . 13 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3635ex 403 . . . . . . . . . . . 12 ((𝜑𝑟𝑅) → (𝑟𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3736reximdva 3226 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3837adantr 474 . . . . . . . . . 10 ((𝜑𝑢𝑈) → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3926, 38mpd 15 . . . . . . . . 9 ((𝜑𝑢𝑈) → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
40 r19.37v 3298 . . . . . . . . 9 (∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4139, 40syl 17 . . . . . . . 8 ((𝜑𝑢𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4241rexlimdva 3241 . . . . . . 7 (𝜑 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4342ad3antrrr 723 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4418, 43mpd 15 . . . . 5 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
4544ralrimiva 3176 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
46 ssfg 22047 . . . . . . . . . . 11 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4722, 46syl 17 . . . . . . . . . 10 (𝜑𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4847, 20syl6sseqr 3878 . . . . . . . . 9 (𝜑𝑅𝑈)
49 ssrexv 3893 . . . . . . . . . 10 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
50 breq 4876 . . . . . . . . . . . . 13 (𝑟 = 𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
5150imbi1d 333 . . . . . . . . . . . 12 (𝑟 = 𝑢 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
52512ralbidv 3199 . . . . . . . . . . 11 (𝑟 = 𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5352cbvrexv 3385 . . . . . . . . . 10 (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
5449, 53syl6ib 243 . . . . . . . . 9 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5548, 54syl 17 . . . . . . . 8 (𝜑 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5655ralimdv 3173 . . . . . . 7 (𝜑 → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5756adantr 474 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
58 nfv 2015 . . . . . . . . . . 11 𝑠(𝜑𝐹:𝑋𝑌)
59 nfra1 3151 . . . . . . . . . . 11 𝑠𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))
6058, 59nfan 2004 . . . . . . . . . 10 𝑠((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
61 nfv 2015 . . . . . . . . . 10 𝑠 𝑣𝑉
6260, 61nfan 2004 . . . . . . . . 9 𝑠(((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉)
63 simp-4r 805 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
64 simplr 787 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑆)
65 rspa 3140 . . . . . . . . . . 11 ((∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
6663, 64, 65syl2anc 581 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
67 simp-4l 803 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (𝜑𝐹:𝑋𝑌))
68 simpr 479 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑣)
69 ssbr 4918 . . . . . . . . . . . . . . . 16 (𝑠𝑣 → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7069adantl 475 . . . . . . . . . . . . . . 15 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7170imim2d 57 . . . . . . . . . . . . . 14 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7271ralimdv 3173 . . . . . . . . . . . . 13 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7372ralimdv 3173 . . . . . . . . . . . 12 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7473reximdv 3225 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7567, 64, 68, 74syl21anc 873 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7666, 75mpd 15 . . . . . . . . 9 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
7710ad3antrrr 723 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
78 simpr 479 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣𝑉)
7978, 13syl6eleq 2917 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆))
80 elfg 22046 . . . . . . . . . . 11 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → (𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆) ↔ (𝑣 ⊆ (𝑌 × 𝑌) ∧ ∃𝑠𝑆 𝑠𝑣)))
8180simplbda 495 . . . . . . . . . 10 ((𝑆 ∈ (fBas‘(𝑌 × 𝑌)) ∧ 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) → ∃𝑠𝑆 𝑠𝑣)
8277, 79, 81syl2anc 581 . . . . . . . . 9 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑠𝑆 𝑠𝑣)
8362, 76, 82r19.29af 3287 . . . . . . . 8 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8483ralrimiva 3176 . . . . . . 7 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8584ex 403 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8657, 85syld 47 . . . . 5 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8786imp 397 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8845, 87impbida 837 . . 3 ((𝜑𝐹:𝑋𝑌) → (∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
8988pm5.32da 576 . 2 (𝜑 → ((𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
904, 89bitrd 271 1 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  wral 3118  wrex 3119  wss 3799   class class class wbr 4874   × cxp 5341  wf 6120  cfv 6124  (class class class)co 6906  fBascfbas 20095  filGencfg 20096  UnifOncust 22374   Cnucucn 22450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-fv 6132  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-map 8125  df-fbas 20104  df-fg 20105  df-ust 22375  df-ucn 22451
This theorem is referenced by:  metucn  22747
  Copyright terms: Public domain W3C validator