Step | Hyp | Ref
| Expression |
1 | | n0 3931 |
. . 3
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
2 | | snssi 4339 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐴 → {𝑧} ⊆ 𝐴) |
3 | 2 | anim2i 593 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴) → ({𝑧} ⊆ 𝑦 ∧ {𝑧} ⊆ 𝐴)) |
4 | | ssin 3835 |
. . . . . . . . . . . 12
⊢ (({𝑧} ⊆ 𝑦 ∧ {𝑧} ⊆ 𝐴) ↔ {𝑧} ⊆ (𝑦 ∩ 𝐴)) |
5 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
6 | 5 | snss 4316 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑦 ∩ 𝐴) ↔ {𝑧} ⊆ (𝑦 ∩ 𝐴)) |
7 | 4, 6 | bitr4i 267 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑦 ∧ {𝑧} ⊆ 𝐴) ↔ 𝑧 ∈ (𝑦 ∩ 𝐴)) |
8 | 3, 7 | sylib 208 |
. . . . . . . . . 10
⊢ (({𝑧} ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ (𝑦 ∩ 𝐴)) |
9 | | ne0i 3921 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑦 ∩ 𝐴) → (𝑦 ∩ 𝐴) ≠ ∅) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (({𝑧} ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴) → (𝑦 ∩ 𝐴) ≠ ∅) |
11 | | inss2 3834 |
. . . . . . . . . . . 12
⊢ (𝑦 ∩ 𝐴) ⊆ 𝐴 |
12 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
13 | 12 | inex1 4799 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∩ 𝐴) ∈ V |
14 | 13 | epfrc 5100 |
. . . . . . . . . . . 12
⊢ (( E Fr
𝐴 ∧ (𝑦 ∩ 𝐴) ⊆ 𝐴 ∧ (𝑦 ∩ 𝐴) ≠ ∅) → ∃𝑥 ∈ (𝑦 ∩ 𝐴)((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) |
15 | 11, 14 | mp3an2 1412 |
. . . . . . . . . . 11
⊢ (( E Fr
𝐴 ∧ (𝑦 ∩ 𝐴) ≠ ∅) → ∃𝑥 ∈ (𝑦 ∩ 𝐴)((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) |
16 | | elin 3796 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑦 ∩ 𝐴) ↔ (𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴)) |
17 | 16 | anbi1i 731 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑦 ∩ 𝐴) ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅)) |
18 | | anass 681 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝑥 ∈ 𝐴 ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅))) |
19 | 17, 18 | bitri 264 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑦 ∩ 𝐴) ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝑥 ∈ 𝐴 ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅))) |
20 | | n0 3931 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∩ 𝐴) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑥 ∩ 𝐴)) |
21 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
22 | 21 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ (𝑥 ∩ 𝐴) → 𝑤 ∈ 𝑥) |
23 | 22 | ancri 575 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (𝑥 ∩ 𝐴) → (𝑤 ∈ 𝑥 ∧ 𝑤 ∈ (𝑥 ∩ 𝐴))) |
24 | | trel 4759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Tr 𝑦 → ((𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑤 ∈ 𝑦)) |
25 | | inass 3823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 ∩ 𝐴) ∩ 𝑥) = (𝑦 ∩ (𝐴 ∩ 𝑥)) |
26 | | incom 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 ∩ 𝑥) = (𝑥 ∩ 𝐴) |
27 | 26 | ineq2i 3811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∩ (𝐴 ∩ 𝑥)) = (𝑦 ∩ (𝑥 ∩ 𝐴)) |
28 | 25, 27 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 ∩ 𝐴) ∩ 𝑥) = (𝑦 ∩ (𝑥 ∩ 𝐴)) |
29 | 28 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ ((𝑦 ∩ 𝐴) ∩ 𝑥) ↔ 𝑤 ∈ (𝑦 ∩ (𝑥 ∩ 𝐴))) |
30 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ (𝑦 ∩ (𝑥 ∩ 𝐴)) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ (𝑥 ∩ 𝐴))) |
31 | 29, 30 | bitr2i 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ 𝑦 ∧ 𝑤 ∈ (𝑥 ∩ 𝐴)) ↔ 𝑤 ∈ ((𝑦 ∩ 𝐴) ∩ 𝑥)) |
32 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ((𝑦 ∩ 𝐴) ∩ 𝑥) → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅) |
33 | 31, 32 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑤 ∈ 𝑦 ∧ 𝑤 ∈ (𝑥 ∩ 𝐴)) → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅) |
34 | 33 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ∈ 𝑦 → (𝑤 ∈ (𝑥 ∩ 𝐴) → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅)) |
35 | 24, 34 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Tr 𝑦 → ((𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → (𝑤 ∈ (𝑥 ∩ 𝐴) → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅))) |
36 | 35 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Tr 𝑦 → (𝑤 ∈ 𝑥 → (𝑥 ∈ 𝑦 → (𝑤 ∈ (𝑥 ∩ 𝐴) → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅)))) |
37 | 36 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Tr 𝑦 → (𝑤 ∈ 𝑥 → (𝑤 ∈ (𝑥 ∩ 𝐴) → (𝑥 ∈ 𝑦 → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅)))) |
38 | 37 | impd 447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Tr 𝑦 → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ (𝑥 ∩ 𝐴)) → (𝑥 ∈ 𝑦 → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅))) |
39 | 23, 38 | syl5 34 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Tr 𝑦 → (𝑤 ∈ (𝑥 ∩ 𝐴) → (𝑥 ∈ 𝑦 → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅))) |
40 | 39 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Tr 𝑦 → (∃𝑤 𝑤 ∈ (𝑥 ∩ 𝐴) → (𝑥 ∈ 𝑦 → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅))) |
41 | 20, 40 | syl5bi 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (Tr 𝑦 → ((𝑥 ∩ 𝐴) ≠ ∅ → (𝑥 ∈ 𝑦 → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅))) |
42 | 41 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ (Tr 𝑦 → (𝑥 ∈ 𝑦 → ((𝑥 ∩ 𝐴) ≠ ∅ → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅))) |
43 | 42 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ ((Tr
𝑦 ∧ 𝑥 ∈ 𝑦) → ((𝑥 ∩ 𝐴) ≠ ∅ → ((𝑦 ∩ 𝐴) ∩ 𝑥) ≠ ∅)) |
44 | 43 | necon4d 2818 |
. . . . . . . . . . . . . . 15
⊢ ((Tr
𝑦 ∧ 𝑥 ∈ 𝑦) → (((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅ → (𝑥 ∩ 𝐴) = ∅)) |
45 | 44 | anim2d 589 |
. . . . . . . . . . . . . 14
⊢ ((Tr
𝑦 ∧ 𝑥 ∈ 𝑦) → ((𝑥 ∈ 𝐴 ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) → (𝑥 ∈ 𝐴 ∧ (𝑥 ∩ 𝐴) = ∅))) |
46 | 45 | expimpd 629 |
. . . . . . . . . . . . 13
⊢ (Tr 𝑦 → ((𝑥 ∈ 𝑦 ∧ (𝑥 ∈ 𝐴 ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅)) → (𝑥 ∈ 𝐴 ∧ (𝑥 ∩ 𝐴) = ∅))) |
47 | 19, 46 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ (Tr 𝑦 → ((𝑥 ∈ (𝑦 ∩ 𝐴) ∧ ((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅) → (𝑥 ∈ 𝐴 ∧ (𝑥 ∩ 𝐴) = ∅))) |
48 | 47 | reximdv2 3014 |
. . . . . . . . . . 11
⊢ (Tr 𝑦 → (∃𝑥 ∈ (𝑦 ∩ 𝐴)((𝑦 ∩ 𝐴) ∩ 𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)) |
49 | 15, 48 | syl5 34 |
. . . . . . . . . 10
⊢ (Tr 𝑦 → (( E Fr 𝐴 ∧ (𝑦 ∩ 𝐴) ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)) |
50 | 49 | expcomd 454 |
. . . . . . . . 9
⊢ (Tr 𝑦 → ((𝑦 ∩ 𝐴) ≠ ∅ → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅))) |
51 | 10, 50 | syl5 34 |
. . . . . . . 8
⊢ (Tr 𝑦 → (({𝑧} ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴) → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅))) |
52 | 51 | expd 452 |
. . . . . . 7
⊢ (Tr 𝑦 → ({𝑧} ⊆ 𝑦 → (𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)))) |
53 | 52 | impcom 446 |
. . . . . 6
⊢ (({𝑧} ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅))) |
54 | 53 | 3adant3 1081 |
. . . . 5
⊢ (({𝑧} ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀𝑤(({𝑧} ⊆ 𝑤 ∧ Tr 𝑤) → 𝑦 ⊆ 𝑤)) → (𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅))) |
55 | | snex 4908 |
. . . . . 6
⊢ {𝑧} ∈ V |
56 | 55 | tz9.1 8605 |
. . . . 5
⊢
∃𝑦({𝑧} ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀𝑤(({𝑧} ⊆ 𝑤 ∧ Tr 𝑤) → 𝑦 ⊆ 𝑤)) |
57 | 54, 56 | exlimiiv 1859 |
. . . 4
⊢ (𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)) |
58 | 57 | exlimiv 1858 |
. . 3
⊢
(∃𝑧 𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)) |
59 | 1, 58 | sylbi 207 |
. 2
⊢ (𝐴 ≠ ∅ → ( E Fr
𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)) |
60 | 59 | impcom 446 |
1
⊢ (( E Fr
𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) |