| Step | Hyp | Ref
| Expression |
| 1 | | wess 5671 |
. . 3
⊢ (𝐵 ⊆ 𝐴 → ( E We 𝐴 → E We 𝐵)) |
| 2 | | n0 4353 |
. . . 4
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
| 3 | | ineq2 4214 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐵 ∩ 𝑥) = (𝐵 ∩ 𝑦)) |
| 4 | 3 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ (𝐵 ∩ 𝑦) = ∅)) |
| 5 | 4 | rspcev 3622 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐵 ∩ 𝑦) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) |
| 6 | 5 | ex 412 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 7 | 6 | adantl 481 |
. . . . . . 7
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 8 | | inss1 4237 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵 |
| 9 | | wefr 5675 |
. . . . . . . . . . . . 13
⊢ ( E We
𝐵 → E Fr 𝐵) |
| 10 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 11 | 10 | inex2 5318 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∩ 𝑦) ∈ V |
| 12 | 11 | epfrc 5670 |
. . . . . . . . . . . . 13
⊢ (( E Fr
𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) |
| 13 | 9, 12 | syl3an1 1164 |
. . . . . . . . . . . 12
⊢ (( E We
𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) |
| 14 | 13 | 3exp 1120 |
. . . . . . . . . . 11
⊢ ( E We
𝐵 → ((𝐵 ∩ 𝑦) ⊆ 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))) |
| 15 | 8, 14 | mpi 20 |
. . . . . . . . . 10
⊢ ( E We
𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)) |
| 16 | | rexin 4250 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
(𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)) |
| 17 | 15, 16 | imbitrdi 251 |
. . . . . . . . 9
⊢ ( E We
𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))) |
| 18 | 17 | adantr 480 |
. . . . . . . 8
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))) |
| 19 | | elin 3967 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (𝐵 ∩ 𝑥) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥)) |
| 20 | | df-3an 1089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵)) |
| 21 | | 3anrot 1100 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
| 22 | 20, 21 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
| 23 | | wetrep 5678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (( E We
𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦)) |
| 24 | 23 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (( E We
𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))) |
| 25 | 22, 24 | sylan2b 594 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (( E We
𝐵 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))) |
| 26 | 25 | exp44 437 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( E We
𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))) |
| 27 | 26 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))) |
| 28 | 27 | com34 91 |
. . . . . . . . . . . . . . . . . 18
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))) |
| 29 | 28 | impd 410 |
. . . . . . . . . . . . . . . . 17
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))) |
| 30 | 19, 29 | biimtrid 242 |
. . . . . . . . . . . . . . . 16
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))) |
| 31 | 30 | imp4a 422 |
. . . . . . . . . . . . . . 15
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦))) |
| 32 | 31 | com23 86 |
. . . . . . . . . . . . . 14
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝑧 ∈ (𝐵 ∩ 𝑥) → 𝑧 ∈ 𝑦))) |
| 33 | 32 | ralrimdv 3152 |
. . . . . . . . . . . . 13
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦)) |
| 34 | | dfss3 3972 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦) |
| 35 | 33, 34 | imbitrrdi 252 |
. . . . . . . . . . . 12
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝐵 ∩ 𝑥) ⊆ 𝑦)) |
| 36 | | dfss 3970 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦)) |
| 37 | | in32 4230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∩ 𝑥) ∩ 𝑦) = ((𝐵 ∩ 𝑦) ∩ 𝑥) |
| 38 | 37 | eqeq2i 2750 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦) ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥)) |
| 39 | 36, 38 | sylbb 219 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥)) |
| 40 | 39 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)) |
| 41 | 40 | biimprd 248 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅)) |
| 42 | 35, 41 | syl6 35 |
. . . . . . . . . . 11
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))) |
| 43 | 42 | expd 415 |
. . . . . . . . . 10
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅)))) |
| 44 | 43 | imp4a 422 |
. . . . . . . . 9
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → ((𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → (𝐵 ∩ 𝑥) = ∅))) |
| 45 | 44 | reximdvai 3165 |
. . . . . . . 8
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 46 | 18, 45 | syld 47 |
. . . . . . 7
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 47 | 7, 46 | pm2.61dne 3028 |
. . . . . 6
⊢ (( E We
𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) |
| 48 | 47 | ex 412 |
. . . . 5
⊢ ( E We
𝐵 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 49 | 48 | exlimdv 1933 |
. . . 4
⊢ ( E We
𝐵 → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 50 | 2, 49 | biimtrid 242 |
. . 3
⊢ ( E We
𝐵 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)) |
| 51 | 1, 50 | syl6com 37 |
. 2
⊢ ( E We
𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))) |
| 52 | 51 | 3imp 1111 |
1
⊢ (( E We
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) |