| Step | Hyp | Ref
| Expression |
| 1 | | pssss 4098 |
. . . . 5
⊢ (𝐹 ⊊ 𝐺 → 𝐹 ⊆ 𝐺) |
| 2 | | dmss 5913 |
. . . . 5
⊢ (𝐹 ⊆ 𝐺 → dom 𝐹 ⊆ dom 𝐺) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹 ⊊ 𝐺 → dom 𝐹 ⊆ dom 𝐺) |
| 4 | 3 | a1i 11 |
. . 3
⊢ (Fun
𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊆ dom 𝐺)) |
| 5 | | pssdif 4369 |
. . . . . . . 8
⊢ (𝐹 ⊊ 𝐺 → (𝐺 ∖ 𝐹) ≠ ∅) |
| 6 | | n0 4353 |
. . . . . . . 8
⊢ ((𝐺 ∖ 𝐹) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝐺 ∖ 𝐹)) |
| 7 | 5, 6 | sylib 218 |
. . . . . . 7
⊢ (𝐹 ⊊ 𝐺 → ∃𝑝 𝑝 ∈ (𝐺 ∖ 𝐹)) |
| 8 | 7 | adantl 481 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → ∃𝑝 𝑝 ∈ (𝐺 ∖ 𝐹)) |
| 9 | | funrel 6583 |
. . . . . . . . . . 11
⊢ (Fun
𝐺 → Rel 𝐺) |
| 10 | | reldif 5825 |
. . . . . . . . . . 11
⊢ (Rel
𝐺 → Rel (𝐺 ∖ 𝐹)) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (Fun
𝐺 → Rel (𝐺 ∖ 𝐹)) |
| 12 | | elrel 5808 |
. . . . . . . . . . . 12
⊢ ((Rel
(𝐺 ∖ 𝐹) ∧ 𝑝 ∈ (𝐺 ∖ 𝐹)) → ∃𝑥∃𝑦 𝑝 = 〈𝑥, 𝑦〉) |
| 13 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝑝 ∈ (𝐺 ∖ 𝐹) ↔ 〈𝑥, 𝑦〉 ∈ (𝐺 ∖ 𝐹))) |
| 14 | | df-br 5144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥(𝐺 ∖ 𝐹)𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝐺 ∖ 𝐹)) |
| 15 | 13, 14 | bitr4di 289 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝑝 ∈ (𝐺 ∖ 𝐹) ↔ 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 16 | 15 | biimpcd 249 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ (𝐺 ∖ 𝐹) → (𝑝 = 〈𝑥, 𝑦〉 → 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((Rel
(𝐺 ∖ 𝐹) ∧ 𝑝 ∈ (𝐺 ∖ 𝐹)) → (𝑝 = 〈𝑥, 𝑦〉 → 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 18 | 17 | 2eximdv 1919 |
. . . . . . . . . . . 12
⊢ ((Rel
(𝐺 ∖ 𝐹) ∧ 𝑝 ∈ (𝐺 ∖ 𝐹)) → (∃𝑥∃𝑦 𝑝 = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 19 | 12, 18 | mpd 15 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐺 ∖ 𝐹) ∧ 𝑝 ∈ (𝐺 ∖ 𝐹)) → ∃𝑥∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦) |
| 20 | 19 | ex 412 |
. . . . . . . . . 10
⊢ (Rel
(𝐺 ∖ 𝐹) → (𝑝 ∈ (𝐺 ∖ 𝐹) → ∃𝑥∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 21 | 11, 20 | syl 17 |
. . . . . . . . 9
⊢ (Fun
𝐺 → (𝑝 ∈ (𝐺 ∖ 𝐹) → ∃𝑥∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 22 | 21 | adantr 480 |
. . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (𝑝 ∈ (𝐺 ∖ 𝐹) → ∃𝑥∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦)) |
| 23 | | difss 4136 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∖ 𝐹) ⊆ 𝐺 |
| 24 | 23 | ssbri 5188 |
. . . . . . . . . . . 12
⊢ (𝑥(𝐺 ∖ 𝐹)𝑦 → 𝑥𝐺𝑦) |
| 25 | 24 | eximi 1835 |
. . . . . . . . . . 11
⊢
(∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦 → ∃𝑦 𝑥𝐺𝑦) |
| 26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦 → ∃𝑦 𝑥𝐺𝑦)) |
| 27 | | brdif 5196 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(𝐺 ∖ 𝐹)𝑦 ↔ (𝑥𝐺𝑦 ∧ ¬ 𝑥𝐹𝑦)) |
| 28 | 27 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (𝑥(𝐺 ∖ 𝐹)𝑦 → ¬ 𝑥𝐹𝑦) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → ¬ 𝑥𝐹𝑦) |
| 30 | 1 | ssbrd 5186 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ⊊ 𝐺 → (𝑥𝐹𝑧 → 𝑥𝐺𝑧)) |
| 31 | 30 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → (𝑥𝐹𝑧 → 𝑥𝐺𝑧)) |
| 32 | | dffun2 6571 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧))) |
| 33 | 32 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
𝐺 → ∀𝑥∀𝑦∀𝑧((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧)) |
| 34 | | 2sp 2186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦∀𝑧((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧) → ((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧)) |
| 35 | 34 | sps 2185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥∀𝑦∀𝑧((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧) → ((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧)) |
| 36 | 33, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Fun
𝐺 → ((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → 𝑦 = 𝑧)) |
| 37 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑦 ↔ 𝑥𝐹𝑧)) |
| 38 | 37 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑧 → 𝑥𝐹𝑦)) |
| 39 | 36, 38 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Fun
𝐺 → ((𝑥𝐺𝑦 ∧ 𝑥𝐺𝑧) → (𝑥𝐹𝑧 → 𝑥𝐹𝑦))) |
| 40 | 39 | expd 415 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝐺 → (𝑥𝐺𝑦 → (𝑥𝐺𝑧 → (𝑥𝐹𝑧 → 𝑥𝐹𝑦)))) |
| 41 | 27 | simplbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥(𝐺 ∖ 𝐹)𝑦 → 𝑥𝐺𝑦) |
| 42 | 40, 41 | impel 505 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐺 ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → (𝑥𝐺𝑧 → (𝑥𝐹𝑧 → 𝑥𝐹𝑦))) |
| 43 | 42 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → (𝑥𝐺𝑧 → (𝑥𝐹𝑧 → 𝑥𝐹𝑦))) |
| 44 | 43 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → (𝑥𝐹𝑧 → (𝑥𝐺𝑧 → 𝑥𝐹𝑦))) |
| 45 | 31, 44 | mpdd 43 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → (𝑥𝐹𝑧 → 𝑥𝐹𝑦)) |
| 46 | 45 | exlimdv 1933 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → (∃𝑧 𝑥𝐹𝑧 → 𝑥𝐹𝑦)) |
| 47 | 29, 46 | mtod 198 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) ∧ 𝑥(𝐺 ∖ 𝐹)𝑦) → ¬ ∃𝑧 𝑥𝐹𝑧) |
| 48 | 47 | ex 412 |
. . . . . . . . . . 11
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (𝑥(𝐺 ∖ 𝐹)𝑦 → ¬ ∃𝑧 𝑥𝐹𝑧)) |
| 49 | 48 | exlimdv 1933 |
. . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦 → ¬ ∃𝑧 𝑥𝐹𝑧)) |
| 50 | 26, 49 | jcad 512 |
. . . . . . . . 9
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦 → (∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))) |
| 51 | 50 | eximdv 1917 |
. . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (∃𝑥∃𝑦 𝑥(𝐺 ∖ 𝐹)𝑦 → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))) |
| 52 | 22, 51 | syld 47 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (𝑝 ∈ (𝐺 ∖ 𝐹) → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))) |
| 53 | 52 | exlimdv 1933 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → (∃𝑝 𝑝 ∈ (𝐺 ∖ 𝐹) → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))) |
| 54 | 8, 53 | mpd 15 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)) |
| 55 | | nss 4048 |
. . . . . 6
⊢ (¬
dom 𝐺 ⊆ dom 𝐹 ↔ ∃𝑥(𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹)) |
| 56 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 57 | 56 | eldm 5911 |
. . . . . . . 8
⊢ (𝑥 ∈ dom 𝐺 ↔ ∃𝑦 𝑥𝐺𝑦) |
| 58 | 56 | eldm 5911 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃𝑧 𝑥𝐹𝑧) |
| 59 | 58 | notbii 320 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ dom 𝐹 ↔ ¬ ∃𝑧 𝑥𝐹𝑧) |
| 60 | 57, 59 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹) ↔ (∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)) |
| 61 | 60 | exbii 1848 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹) ↔ ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)) |
| 62 | 55, 61 | bitri 275 |
. . . . 5
⊢ (¬
dom 𝐺 ⊆ dom 𝐹 ↔ ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)) |
| 63 | 54, 62 | sylibr 234 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐹 ⊊ 𝐺) → ¬ dom 𝐺 ⊆ dom 𝐹) |
| 64 | 63 | ex 412 |
. . 3
⊢ (Fun
𝐺 → (𝐹 ⊊ 𝐺 → ¬ dom 𝐺 ⊆ dom 𝐹)) |
| 65 | 4, 64 | jcad 512 |
. 2
⊢ (Fun
𝐺 → (𝐹 ⊊ 𝐺 → (dom 𝐹 ⊆ dom 𝐺 ∧ ¬ dom 𝐺 ⊆ dom 𝐹))) |
| 66 | | dfpss3 4089 |
. 2
⊢ (dom
𝐹 ⊊ dom 𝐺 ↔ (dom 𝐹 ⊆ dom 𝐺 ∧ ¬ dom 𝐺 ⊆ dom 𝐹)) |
| 67 | 65, 66 | imbitrrdi 252 |
1
⊢ (Fun
𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺)) |