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

Theorem isucn2 21996
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 21995 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
41, 2, 3syl2anc 692 . 2 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
5 isucn2.4 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
6 ssfg 21589 . . . . . . . . . . . 12 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
75, 6syl 17 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆))
8 isucn2.v . . . . . . . . . . 11 𝑉 = ((𝑌 × 𝑌)filGen𝑆)
97, 8syl6sseqr 3633 . . . . . . . . . 10 (𝜑𝑆𝑉)
109adantr 481 . . . . . . . . 9 ((𝜑𝐹:𝑋𝑌) → 𝑆𝑉)
1110adantr 481 . . . . . . . 8 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → 𝑆𝑉)
1211sselda 3584 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → 𝑠𝑉)
13 simplr 791 . . . . . . 7 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
14 breq 4617 . . . . . . . . . . 11 (𝑣 = 𝑠 → ((𝐹𝑥)𝑣(𝐹𝑦) ↔ (𝐹𝑥)𝑠(𝐹𝑦)))
1514imbi2d 330 . . . . . . . . . 10 (𝑣 = 𝑠 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
1615ralbidv 2980 . . . . . . . . 9 (𝑣 = 𝑠 → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
1716rexralbidv 3051 . . . . . . . 8 (𝑣 = 𝑠 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
1817rspcva 3293 . . . . . . 7 ((𝑠𝑉 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
1912, 13, 18syl2anc 692 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
20 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → 𝑢𝑈)
21 isucn2.u . . . . . . . . . . . 12 𝑈 = ((𝑋 × 𝑋)filGen𝑅)
2220, 21syl6eleq 2708 . . . . . . . . . . 11 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅))
23 isucn2.3 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ (fBas‘(𝑋 × 𝑋)))
24 elfg 21588 . . . . . . . . . . . . 13 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2523, 24syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟𝑅 𝑟𝑢)))
2625simplbda 653 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) → ∃𝑟𝑅 𝑟𝑢)
2722, 26syldan 487 . . . . . . . . . 10 ((𝜑𝑢𝑈) → ∃𝑟𝑅 𝑟𝑢)
28 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑢𝑟𝑢)
2928ssbrd 4658 . . . . . . . . . . . . . . . . . 18 (𝑟𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
3029imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑟𝑢 → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3130adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3231ralrimivw 2961 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3332ralrimivw 2961 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → ∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
34 ralim 2943 . . . . . . . . . . . . . . 15 (∀𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3534ralimi 2947 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑋 ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
36 ralim 2943 . . . . . . . . . . . . . 14 (∀𝑥𝑋 (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3733, 35, 363syl 18 . . . . . . . . . . . . 13 (((𝜑𝑟𝑅) ∧ 𝑟𝑢) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
3837ex 450 . . . . . . . . . . . 12 ((𝜑𝑟𝑅) → (𝑟𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
3938reximdva 3011 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
4039adantr 481 . . . . . . . . . 10 ((𝜑𝑢𝑈) → (∃𝑟𝑅 𝑟𝑢 → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
4127, 40mpd 15 . . . . . . . . 9 ((𝜑𝑢𝑈) → ∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
42 r19.37v 3079 . . . . . . . . 9 (∃𝑟𝑅 (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4341, 42syl 17 . . . . . . . 8 ((𝜑𝑢𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4443rexlimdva 3024 . . . . . . 7 (𝜑 → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4544ad3antrrr 765 . . . . . 6 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
4619, 45mpd 15 . . . . 5 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ∧ 𝑠𝑆) → ∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
4746ralrimiva 2960 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) → ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
48 ssfg 21589 . . . . . . . . . . 11 (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
4923, 48syl 17 . . . . . . . . . 10 (𝜑𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅))
5049, 21syl6sseqr 3633 . . . . . . . . 9 (𝜑𝑅𝑈)
51 ssrexv 3648 . . . . . . . . . 10 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
52 breq 4617 . . . . . . . . . . . . 13 (𝑟 = 𝑢 → (𝑥𝑟𝑦𝑥𝑢𝑦))
5352imbi1d 331 . . . . . . . . . . . 12 (𝑟 = 𝑢 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
54532ralbidv 2983 . . . . . . . . . . 11 (𝑟 = 𝑢 → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5554cbvrexv 3160 . . . . . . . . . 10 (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ↔ ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
5651, 55syl6ib 241 . . . . . . . . 9 (𝑅𝑈 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5750, 56syl 17 . . . . . . . 8 (𝜑 → (∃𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5857ralimdv 2957 . . . . . . 7 (𝜑 → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
5958adantr 481 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
60 nfv 1840 . . . . . . . . . . 11 𝑠(𝜑𝐹:𝑋𝑌)
61 nfra1 2936 . . . . . . . . . . 11 𝑠𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))
6260, 61nfan 1825 . . . . . . . . . 10 𝑠((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
63 nfv 1840 . . . . . . . . . 10 𝑠 𝑣𝑉
6462, 63nfan 1825 . . . . . . . . 9 𝑠(((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉)
65 simp-4r 806 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
66 simplr 791 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑆)
67 rspa 2925 . . . . . . . . . . 11 ((∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) ∧ 𝑠𝑆) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
6865, 66, 67syl2anc 692 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))
69 simp-4l 805 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (𝜑𝐹:𝑋𝑌))
70 simpr 477 . . . . . . . . . . 11 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → 𝑠𝑣)
71 id 22 . . . . . . . . . . . . . . . . 17 (𝑠𝑣𝑠𝑣)
7271ssbrd 4658 . . . . . . . . . . . . . . . 16 (𝑠𝑣 → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7372adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝐹𝑥)𝑠(𝐹𝑦) → (𝐹𝑥)𝑣(𝐹𝑦)))
7473imim2d 57 . . . . . . . . . . . . . 14 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ((𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7574ralimdv 2957 . . . . . . . . . . . . 13 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7675ralimdv 2957 . . . . . . . . . . . 12 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7776reximdv 3010 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7869, 66, 70, 77syl21anc 1322 . . . . . . . . . 10 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → (∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
7968, 78mpd 15 . . . . . . . . 9 ((((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) ∧ 𝑠𝑆) ∧ 𝑠𝑣) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
805ad3antrrr 765 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))
81 simpr 477 . . . . . . . . . . 11 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣𝑉)
8281, 8syl6eleq 2708 . . . . . . . . . 10 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆))
83 elfg 21588 . . . . . . . . . . 11 (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → (𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆) ↔ (𝑣 ⊆ (𝑌 × 𝑌) ∧ ∃𝑠𝑆 𝑠𝑣)))
8483simplbda 653 . . . . . . . . . 10 ((𝑆 ∈ (fBas‘(𝑌 × 𝑌)) ∧ 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) → ∃𝑠𝑆 𝑠𝑣)
8580, 82, 84syl2anc 692 . . . . . . . . 9 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑠𝑆 𝑠𝑣)
8664, 79, 85r19.29af 3069 . . . . . . . 8 ((((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) ∧ 𝑣𝑉) → ∃𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8786ralrimiva 2960 . . . . . . 7 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
8887ex 450 . . . . . 6 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
8959, 88syld 47 . . . . 5 ((𝜑𝐹:𝑋𝑌) → (∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))))
9089imp 445 . . . 4 (((𝜑𝐹:𝑋𝑌) ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))) → ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))
9147, 90impbida 876 . . 3 ((𝜑𝐹:𝑋𝑌) → (∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)) ↔ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦))))
9291pm5.32da 672 . 2 (𝜑 → ((𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑢𝑈𝑥𝑋𝑦𝑋 (𝑥𝑢𝑦 → (𝐹𝑥)𝑣(𝐹𝑦))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
934, 92bitrd 268 1 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑠𝑆𝑟𝑅𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑠(𝐹𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  wss 3556   class class class wbr 4615   × cxp 5074  wf 5845  cfv 5849  (class class class)co 6607  fBascfbas 19656  filGencfg 19657  UnifOncust 21916   Cnucucn 21992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-map 7807  df-fbas 19665  df-fg 19666  df-ust 21917  df-ucn 21993
This theorem is referenced by:  metucn  22289
  Copyright terms: Public domain W3C validator