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

Theorem isucn2 22293
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 22292 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
41, 2, 3syl2anc 575 . 2 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
5 breq 4846 . . . . . . . . . 10 (𝑣 = 𝑠 → ((𝐹𝑥)𝑣(𝐹𝑦) ↔ (𝐹𝑥)𝑠(𝐹𝑦)))
65imbi2d 331 . . . . . . . . 9 (𝑣 = 𝑠 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
76ralbidv 3174 . . . . . . . 8 (𝑣 = 𝑠 → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
87rexralbidv 3246 . . . . . . 7 (𝑣 = 𝑠 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
9 simplr 776 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
10 isucn2.4 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
11 ssfg 21886 . . . . . . . . . . . 12 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
1210, 11syl 17 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
13 isucn2.v . . . . . . . . . . 11 𝑉 = ((𝑌 × 𝑌)filGen𝑆)
1412, 13syl6sseqr 3849 . . . . . . . . . 10 (𝜑𝑆𝑉)
1514adantr 468 . . . . . . . . 9 ((𝜑𝐹:𝑋𝑌) → 𝑆𝑉)
1615adantr 468 . . . . . . . 8 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → 𝑆𝑉)
1716sselda 3798 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → 𝑠𝑉)
188, 9, 17rspcdva 3508 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
19 simpr 473 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → 𝑢𝑈)
20 isucn2.u . . . . . . . . . . . 12 𝑈 = ((𝑋 × 𝑋)filGen𝑅)
2119, 20syl6eleq 2895 . . . . . . . . . . 11 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅))
22 isucn2.3 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ (fBas‘(𝑋 × 𝑋)))
23 elfg 21885 . . . . . . . . . . . . 13 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2422, 23syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2524simplbda 489 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) → ∃𝑟𝑅 𝑟𝑢)
2621, 25syldan 581 . . . . . . . . . 10 ((𝜑𝑢𝑈) → ∃𝑟𝑅 𝑟𝑢)
27 ssbr 4888 . . . . . . . . . . . . . . . . . 18 (𝑟𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
2827imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑟𝑢 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
2928adantl 469 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3029ralrimivw 3155 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3130ralrimivw 3155 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
32 ralim 3136 . . . . . . . . . . . . . . 15 (∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3332ralimi 3140 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
34 ralim 3136 . . . . . . . . . . . . . 14 (∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3531, 33, 343syl 18 . . . . . . . . . . . . 13 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3635ex 399 . . . . . . . . . . . 12 ((𝜑𝑟𝑅) → (𝑟𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3736reximdva 3204 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3837adantr 468 . . . . . . . . . 10 ((𝜑𝑢𝑈) → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3926, 38mpd 15 . . . . . . . . 9 ((𝜑𝑢𝑈) → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
40 r19.37v 3275 . . . . . . . . 9 (∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4139, 40syl 17 . . . . . . . 8 ((𝜑𝑢𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4241rexlimdva 3219 . . . . . . 7 (𝜑 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4342ad3antrrr 712 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4418, 43mpd 15 . . . . 5 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
4544ralrimiva 3154 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
46 ssfg 21886 . . . . . . . . . . 11 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4722, 46syl 17 . . . . . . . . . 10 (𝜑𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4847, 20syl6sseqr 3849 . . . . . . . . 9 (𝜑𝑅𝑈)
49 ssrexv 3864 . . . . . . . . . 10 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
50 breq 4846 . . . . . . . . . . . . 13 (𝑟 = 𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
5150imbi1d 332 . . . . . . . . . . . 12 (𝑟 = 𝑢 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
52512ralbidv 3177 . . . . . . . . . . 11 (𝑟 = 𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5352cbvrexv 3361 . . . . . . . . . 10 (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
5449, 53syl6ib 242 . . . . . . . . 9 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5548, 54syl 17 . . . . . . . 8 (𝜑 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5655ralimdv 3151 . . . . . . 7 (𝜑 → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5756adantr 468 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
58 nfv 2005 . . . . . . . . . . 11 𝑠(𝜑𝐹:𝑋𝑌)
59 nfra1 3129 . . . . . . . . . . 11 𝑠𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))
6058, 59nfan 1990 . . . . . . . . . 10 𝑠((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
61 nfv 2005 . . . . . . . . . 10 𝑠 𝑣𝑉
6260, 61nfan 1990 . . . . . . . . 9 𝑠(((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉)
63 simp-4r 794 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
64 simplr 776 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑆)
65 rspa 3118 . . . . . . . . . . 11 ((∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
6663, 64, 65syl2anc 575 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
67 simp-4l 792 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (𝜑𝐹:𝑋𝑌))
68 simpr 473 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑣)
69 ssbr 4888 . . . . . . . . . . . . . . . 16 (𝑠𝑣 → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7069adantl 469 . . . . . . . . . . . . . . 15 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7170imim2d 57 . . . . . . . . . . . . . 14 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7271ralimdv 3151 . . . . . . . . . . . . 13 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7372ralimdv 3151 . . . . . . . . . . . 12 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7473reximdv 3203 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7567, 64, 68, 74syl21anc 857 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7666, 75mpd 15 . . . . . . . . 9 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
7710ad3antrrr 712 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
78 simpr 473 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣𝑉)
7978, 13syl6eleq 2895 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆))
80 elfg 21885 . . . . . . . . . . 11 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → (𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆) ↔ (𝑣 ⊆ (𝑌 × 𝑌) ∧ ∃𝑠𝑆 𝑠𝑣)))
8180simplbda 489 . . . . . . . . . 10 ((𝑆 ∈ (fBas‘(𝑌 × 𝑌)) ∧ 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) → ∃𝑠𝑆 𝑠𝑣)
8277, 79, 81syl2anc 575 . . . . . . . . 9 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑠𝑆 𝑠𝑣)
8362, 76, 82r19.29af 3264 . . . . . . . 8 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8483ralrimiva 3154 . . . . . . 7 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8584ex 399 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8657, 85syld 47 . . . . 5 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8786imp 395 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8845, 87impbida 826 . . 3 ((𝜑𝐹:𝑋𝑌) → (∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
8988pm5.32da 570 . 2 (𝜑 → ((𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
904, 89bitrd 270 1 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wral 3096  wrex 3097  wss 3769   class class class wbr 4844   × cxp 5309  wf 6093  cfv 6097  (class class class)co 6870  fBascfbas 19938  filGencfg 19939  UnifOncust 22213   Cnucucn 22289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-map 8090  df-fbas 19947  df-fg 19948  df-ust 22214  df-ucn 22290
This theorem is referenced by:  metucn  22586
  Copyright terms: Public domain W3C validator