| Step | Hyp | Ref
| Expression |
| 1 | | breq 5145 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝐹‘𝑥)𝑤(𝐹‘𝑦) ↔ (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
| 2 | 1 | imbi2d 340 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) ↔ (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
| 3 | 2 | ralbidv 3178 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
| 4 | 3 | rexralbidv 3223 |
. . . . 5
⊢ (𝑤 = 𝑊 → (∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)) ↔ ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
| 5 | | ucnprima.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) |
| 6 | | ucnprima.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) |
| 7 | | ucnprima.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) |
| 8 | | isucn 24287 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦))))) |
| 9 | 6, 7, 8 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦))))) |
| 10 | 5, 9 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝑋⟶𝑌 ∧ ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦)))) |
| 11 | 10 | simprd 495 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑤(𝐹‘𝑦))) |
| 12 | | ucnprima.4 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
| 13 | 4, 11, 12 | rspcdva 3623 |
. . . 4
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
| 14 | | simplll 775 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → 𝜑) |
| 15 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
| 16 | | ustssxp 24213 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑟 ∈ 𝑈) → 𝑟 ⊆ (𝑋 × 𝑋)) |
| 17 | 6, 16 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → 𝑟 ⊆ (𝑋 × 𝑋)) |
| 18 | 17 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ 𝑝 ∈ 𝑟) → 𝑝 ∈ (𝑋 × 𝑋)) |
| 19 | 18 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → 𝑝 ∈ (𝑋 × 𝑋)) |
| 20 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → 𝑝 ∈ 𝑟) |
| 21 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → 𝑝 ∈ (𝑋 × 𝑋)) |
| 23 | | elxp2 5709 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉) |
| 24 | 22, 23 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉) |
| 25 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 = 〈𝑥, 𝑦〉) |
| 26 | 25 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑝 ∈ 𝑟 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟)) |
| 27 | 26 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑝 ∈ 𝑟 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟)) |
| 28 | | df-br 5144 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑟𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟) |
| 29 | 27, 28 | bitr4di 289 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑝 ∈ 𝑟 ↔ 𝑥𝑟𝑦)) |
| 30 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 ∈ (𝑋 × 𝑋)) |
| 31 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 ∈
V |
| 32 | | ucnprima.5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
| 33 | 6, 7, 5, 12, 32 | ucnimalem 24289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
| 34 | 33 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ (𝑋 × 𝑋) ∧ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 ∈ V) → (𝐺‘𝑝) = 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
| 35 | 30, 31, 34 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐺‘𝑝) = 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 = 〈𝑥, 𝑦〉) |
| 37 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 ∈ (𝑋 × 𝑋) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
| 38 | 30, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
| 39 | 36, 38 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 〈𝑥, 𝑦〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
| 40 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑥 ∈ V |
| 41 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑦 ∈ V |
| 42 | 40, 41 | opth 5481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑥, 𝑦〉 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ↔
(𝑥 = (1st
‘𝑝) ∧ 𝑦 = (2nd ‘𝑝))) |
| 43 | 39, 42 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝑥 = (1st ‘𝑝) ∧ 𝑦 = (2nd ‘𝑝))) |
| 44 | 43 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑥 = (1st ‘𝑝)) |
| 45 | 44 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐹‘𝑥) = (𝐹‘(1st ‘𝑝))) |
| 46 | 43 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 𝑦 = (2nd ‘𝑝)) |
| 47 | 46 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐹‘𝑦) = (𝐹‘(2nd ‘𝑝))) |
| 48 | 45, 47 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
| 49 | 35, 48 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → (𝐺‘𝑝) = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
| 50 | 49 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑝) ∈ 𝑊 ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ 𝑊)) |
| 51 | | df-br 5144 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥)𝑊(𝐹‘𝑦) ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ 𝑊) |
| 52 | 50, 51 | bitr4di 289 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑝) ∈ 𝑊 ↔ (𝐹‘𝑥)𝑊(𝐹‘𝑦))) |
| 53 | 29, 52 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = 〈𝑥, 𝑦〉) → ((𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊) ↔ (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)))) |
| 54 | 53 | exbiri 811 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 = 〈𝑥, 𝑦〉 → ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
| 55 | 54 | reximdv 3170 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉 → ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
| 56 | 55 | reximdv 3170 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑝 = 〈𝑥, 𝑦〉 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
| 57 | 24, 56 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) |
| 58 | 57 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) |
| 59 | 21, 58 | r19.29d2r 3140 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)))) |
| 60 | | pm3.35 803 |
. . . . . . . . . . . 12
⊢ (((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
| 61 | 60 | rexlimivw 3151 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
| 62 | 61 | rexlimivw 3151 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊))) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
| 63 | 59, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 ∈ 𝑟 → (𝐺‘𝑝) ∈ 𝑊)) |
| 64 | 63 | imp 406 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 ∈ 𝑟) → (𝐺‘𝑝) ∈ 𝑊) |
| 65 | 14, 15, 19, 20, 64 | syl1111anc 841 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) ∧ 𝑝 ∈ 𝑟) → (𝐺‘𝑝) ∈ 𝑊) |
| 66 | 65 | ralrimiva 3146 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑈) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦))) → ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊) |
| 67 | 66 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
| 68 | 67 | reximdva 3168 |
. . . 4
⊢ (𝜑 → (∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑊(𝐹‘𝑦)) → ∃𝑟 ∈ 𝑈 ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
| 69 | 13, 68 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊) |
| 70 | 32 | mpofun 7557 |
. . . . . 6
⊢ Fun 𝐺 |
| 71 | | opex 5469 |
. . . . . . . 8
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
| 72 | 32, 71 | dmmpo 8096 |
. . . . . . 7
⊢ dom 𝐺 = (𝑋 × 𝑋) |
| 73 | 17, 72 | sseqtrrdi 4025 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → 𝑟 ⊆ dom 𝐺) |
| 74 | | funimass4 6973 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝑟 ⊆ dom 𝐺) → ((𝐺 “ 𝑟) ⊆ 𝑊 ↔ ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
| 75 | 70, 73, 74 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → ((𝐺 “ 𝑟) ⊆ 𝑊 ↔ ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊)) |
| 76 | 75 | biimprd 248 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑈) → (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) |
| 77 | 76 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) |
| 78 | | r19.29r 3116 |
. . 3
⊢
((∃𝑟 ∈
𝑈 ∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ ∀𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) → ∃𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊))) |
| 79 | 69, 77, 78 | syl2anc 584 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊))) |
| 80 | | pm3.35 803 |
. . 3
⊢
((∀𝑝 ∈
𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) → (𝐺 “ 𝑟) ⊆ 𝑊) |
| 81 | 80 | reximi 3084 |
. 2
⊢
(∃𝑟 ∈
𝑈 (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 ∧ (∀𝑝 ∈ 𝑟 (𝐺‘𝑝) ∈ 𝑊 → (𝐺 “ 𝑟) ⊆ 𝑊)) → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) |
| 82 | 79, 81 | syl 17 |
1
⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) |