Step | Hyp | Ref
| Expression |
1 | | ucnprima.4 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
2 | | ucnprima.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) |
3 | | ucnprima.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) |
4 | | ucnprima.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) |
5 | | isucn 21892 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦))))) |
6 | 3, 4, 5 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦))))) |
7 | 2, 6 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝑋⟶𝑌 ∧ ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)))) |
8 | 7 | simprd 478 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦))) |
9 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((𝐹‘𝑥)𝑤(𝐹‘𝑦) ↔ (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
10 | 9 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) ↔ (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
11 | 10 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
12 | 11 | rexralbidv 3040 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) ↔ ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
13 | 12 | rspcv 3278 |
. . . . 5
⊢ (𝑊 ∈ 𝑉 → (∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
14 | 1, 8, 13 | sylc 63 |
. . . 4
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
15 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → 𝜑) |
16 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
17 | 15, 16 | jca 553 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → (𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
18 | | ustssxp 21818 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑟 ∈ 𝑈) → 𝑟 ⊆ (𝑋 × 𝑋)) |
19 | 3, 18 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → 𝑟 ⊆ (𝑋 × 𝑋)) |
20 | 19 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ 𝑝 ∈ 𝑟) → 𝑝 ∈ (𝑋 × 𝑋)) |
21 | 20 | adantlr 747 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → 𝑝 ∈ (𝑋 × 𝑋)) |
22 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → 𝑝 ∈ 𝑟) |
23 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
24 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → 𝑝 ∈ (𝑋 × 𝑋)) |
25 | | elxp2 5056 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉) |
26 | 24, 25 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉) |
27 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 = 〈𝑥, 𝑦〉) |
28 | 27 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑝 ∈ 𝑟 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟)) |
29 | 28 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑝 ∈ 𝑟 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟)) |
30 | | df-br 4584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑟𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟) |
31 | 29, 30 | syl6bbr 277 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑝 ∈ 𝑟 ↔ 𝑥𝑟𝑦)) |
32 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 ∈ (𝑋 × 𝑋)) |
33 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 ∈
V |
34 | | ucnprima.5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
35 | 3, 4, 2, 1, 34 | ucnimalem 21894 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
36 | 35 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ (𝑋 × 𝑋) ∧ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 ∈ V) → (𝐺‘𝑝) = 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
37 | 32, 33, 36 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐺‘𝑝) = 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
38 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 = 〈𝑥, 𝑦〉) |
39 | | 1st2nd2 7096 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 ∈ (𝑋 × 𝑋) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
40 | 32, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
41 | 38, 40 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 〈𝑥, 𝑦〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
42 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑥 ∈ V |
43 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑦 ∈ V |
44 | 42, 43 | opth 4871 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑥, 𝑦〉 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ↔
(𝑥 = (1st
‘𝑝) ∧ 𝑦 = (2nd ‘𝑝))) |
45 | 41, 44 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑥 = (1st ‘𝑝) ∧ 𝑦 = (2nd ‘𝑝))) |
46 | 45 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑥 = (1st ‘𝑝)) |
47 | 46 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐹‘𝑥) = (𝐹‘(1st ‘𝑝))) |
48 | 45 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑦 = (2nd ‘𝑝)) |
49 | 48 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐹‘𝑦) = (𝐹‘(2nd ‘𝑝))) |
50 | 47, 49 | opeq12d 4348 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
51 | 37, 50 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐺‘𝑝) = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
52 | 51 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑝) ∈ 𝑊 ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ 𝑊)) |
53 | | df-br 4584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥)𝑊(𝐹‘𝑦) ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ 𝑊) |
54 | 52, 53 | syl6bbr 277 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑝) ∈ 𝑊 ↔ (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
55 | 31, 54 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → ((𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊) ↔ (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
56 | 55 | exbiri 650 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 = 〈𝑥, 𝑦〉 → ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
57 | 56 | reximdv 2999 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉 → ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
58 | 57 | reximdv 2999 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
59 | 26, 58 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) |
60 | 59 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) |
61 | 23, 60 | r19.29d2r 3061 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
62 | | pm3.35 609 |
. . . . . . . . . . . 12
⊢ (((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
63 | 62 | rexlimivw 3011 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
64 | 63 | rexlimivw 3011 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
65 | 61, 64 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
66 | 65 | imp 444 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 ∈ 𝑟) → (𝐺‘𝑝) ∈ 𝑊) |
67 | 17, 21, 22, 66 | syl21anc 1317 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → (𝐺‘𝑝) ∈ 𝑊) |
68 | 67 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) → ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊) |
69 | 68 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
70 | 69 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑈 ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
71 | 14, 70 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊) |
72 | 34 | mpt2fun 6660 |
. . . . . 6
⊢ Fun 𝐺 |
73 | | opex 4859 |
. . . . . . . 8
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
74 | 34, 73 | dmmpt2 7129 |
. . . . . . 7
⊢ dom 𝐺 = (𝑋 × 𝑋) |
75 | 19, 74 | syl6sseqr 3615 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → 𝑟 ⊆ dom 𝐺) |
76 | | funimass4 6157 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝑟 ⊆ dom 𝐺) → ((𝐺 “ 𝑟) ⊆ 𝑊 ↔ ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
77 | 72, 75, 76 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → ((𝐺 “ 𝑟) ⊆ 𝑊 ↔ ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
78 | 77 | biimprd 237 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) |
79 | 78 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) |
80 | | r19.29r 3055 |
. . 3
⊢
((∃𝑟 ∈
𝑈 ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ ∀𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) → ∃𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊))) |
81 | 71, 79, 80 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊))) |
82 | | pm3.35 609 |
. . 3
⊢
((∀𝑝 ∈
𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) → (𝐺 “ 𝑟) ⊆ 𝑊) |
83 | 82 | reximi 2994 |
. 2
⊢
(∃𝑟 ∈
𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) |
84 | 81, 83 | syl 17 |
1
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) |