Step | Hyp | Ref
| Expression |
1 | | isucn2.1 |
. . 3
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) |
2 | | isucn2.2 |
. . 3
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) |
3 | | isucn 23175 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
4 | 1, 2, 3 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
5 | | breq 5055 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑠 → ((𝐹‘𝑥)𝑣(𝐹‘𝑦) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
6 | 5 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑣 = 𝑠 → ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
7 | 6 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑣 = 𝑠 → (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
8 | 7 | rexralbidv 3220 |
. . . . . . 7
⊢ (𝑣 = 𝑠 → (∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
9 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ∧ 𝑠 ∈ 𝑆) → ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
10 | | isucn2.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ (fBas‘(𝑌 × 𝑌))) |
11 | | ssfg 22769 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆ ((𝑌 × 𝑌)filGen𝑆)) |
13 | | isucn2.v |
. . . . . . . . . . 11
⊢ 𝑉 = ((𝑌 × 𝑌)filGen𝑆) |
14 | 12, 13 | sseqtrrdi 3952 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ 𝑉) |
15 | 14 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → 𝑆 ⊆ 𝑉) |
16 | 15 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) → 𝑆 ⊆ 𝑉) |
17 | 16 | sselda 3901 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑉) |
18 | 8, 9, 17 | rspcdva 3539 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ∧ 𝑠 ∈ 𝑆) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
19 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈) |
20 | | isucn2.u |
. . . . . . . . . . . 12
⊢ 𝑈 = ((𝑋 × 𝑋)filGen𝑅) |
21 | 19, 20 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) |
22 | | isucn2.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ (fBas‘(𝑋 × 𝑋))) |
23 | | elfg 22768 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅) ↔ (𝑢 ⊆ (𝑋 × 𝑋) ∧ ∃𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢))) |
25 | 24 | simplbda 503 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑋 × 𝑋)filGen𝑅)) → ∃𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢) |
26 | 21, 25 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∃𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢) |
27 | | ssbr 5097 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ⊆ 𝑢 → (𝑥𝑟𝑦 → 𝑥𝑢𝑦)) |
28 | 27 | imim1d 82 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ⊆ 𝑢 → ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
29 | 28 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ 𝑟 ⊆ 𝑢) → ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
30 | 29 | ralrimivw 3106 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ 𝑟 ⊆ 𝑢) → ∀𝑦 ∈ 𝑋 ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
31 | 30 | ralrimivw 3106 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ 𝑟 ⊆ 𝑢) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
32 | | ralim 3085 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝑋 ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) → (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
33 | 32 | ralimi 3083 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) → ∀𝑥 ∈ 𝑋 (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
34 | | ralim 3085 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑋 (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ 𝑟 ⊆ 𝑢) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
36 | 35 | ex 416 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 ⊆ 𝑢 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) |
37 | 36 | reximdva 3193 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 → ∃𝑟 ∈ 𝑅 (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) |
38 | 37 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∃𝑟 ∈ 𝑅 𝑟 ⊆ 𝑢 → ∃𝑟 ∈ 𝑅 (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) |
39 | 26, 38 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∃𝑟 ∈ 𝑅 (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
40 | | r19.37v 3258 |
. . . . . . . . 9
⊢
(∃𝑟 ∈
𝑅 (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
42 | 41 | rexlimdva 3203 |
. . . . . . 7
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
43 | 42 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ∧ 𝑠 ∈ 𝑆) → (∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
44 | 18, 43 | mpd 15 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ∧ 𝑠 ∈ 𝑆) → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
45 | 44 | ralrimiva 3105 |
. . . 4
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) → ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
46 | | ssfg 22769 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (fBas‘(𝑋 × 𝑋)) → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅)) |
47 | 22, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ⊆ ((𝑋 × 𝑋)filGen𝑅)) |
48 | 47, 20 | sseqtrrdi 3952 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ 𝑈) |
49 | | ssrexv 3968 |
. . . . . . . . . 10
⊢ (𝑅 ⊆ 𝑈 → (∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
50 | | breq 5055 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑢 → (𝑥𝑟𝑦 ↔ 𝑥𝑢𝑦)) |
51 | 50 | imbi1d 345 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑢 → ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
52 | 51 | 2ralbidv 3120 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑢 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
53 | 52 | cbvrexvw 3359 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) ↔ ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
54 | 49, 53 | syl6ib 254 |
. . . . . . . . 9
⊢ (𝑅 ⊆ 𝑈 → (∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
55 | 48, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
56 | 55 | ralimdv 3101 |
. . . . . . 7
⊢ (𝜑 → (∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
57 | 56 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
58 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠(𝜑 ∧ 𝐹:𝑋⟶𝑌) |
59 | | nfra1 3140 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) |
60 | 58, 59 | nfan 1907 |
. . . . . . . . . 10
⊢
Ⅎ𝑠((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
61 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑠 𝑣 ∈ 𝑉 |
62 | 60, 61 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑠(((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) |
63 | | rspa 3128 |
. . . . . . . . . . 11
⊢
((∀𝑠 ∈
𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) ∧ 𝑠 ∈ 𝑆) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
64 | 63 | ad5ant24 761 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) |
65 | | simp-4l 783 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → (𝜑 ∧ 𝐹:𝑋⟶𝑌)) |
66 | | simplr 769 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → 𝑠 ∈ 𝑆) |
67 | | simpr 488 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → 𝑠 ⊆ 𝑣) |
68 | | ssbr 5097 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ⊆ 𝑣 → ((𝐹‘𝑥)𝑠(𝐹‘𝑦) → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
69 | 68 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → ((𝐹‘𝑥)𝑠(𝐹‘𝑦) → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
70 | 69 | imim2d 57 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
71 | 70 | ralimdv 3101 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
72 | 71 | ralimdv 3101 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
73 | 72 | reximdv 3192 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → (∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
74 | 65, 66, 67, 73 | syl21anc 838 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → (∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
75 | 64, 74 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) ∧ 𝑠 ∈ 𝑆) ∧ 𝑠 ⊆ 𝑣) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
76 | 10 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) → 𝑆 ∈ (fBas‘(𝑌 × 𝑌))) |
77 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
78 | 77, 13 | eleqtrdi 2848 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) |
79 | | elfg 22768 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (fBas‘(𝑌 × 𝑌)) → (𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆) ↔ (𝑣 ⊆ (𝑌 × 𝑌) ∧ ∃𝑠 ∈ 𝑆 𝑠 ⊆ 𝑣))) |
80 | 79 | simplbda 503 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (fBas‘(𝑌 × 𝑌)) ∧ 𝑣 ∈ ((𝑌 × 𝑌)filGen𝑆)) → ∃𝑠 ∈ 𝑆 𝑠 ⊆ 𝑣) |
81 | 76, 78, 80 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) → ∃𝑠 ∈ 𝑆 𝑠 ⊆ 𝑣) |
82 | 62, 75, 81 | r19.29af 3249 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) ∧ 𝑣 ∈ 𝑉) → ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
83 | 82 | ralrimiva 3105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) → ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
84 | 83 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
85 | 57, 84 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)) → ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))) |
86 | 85 | imp 410 |
. . . 4
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))) → ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) |
87 | 45, 86 | impbida 801 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))) |
88 | 87 | pm5.32da 582 |
. 2
⊢ (𝜑 → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑢 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) |
89 | 4, 88 | bitrd 282 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) |