Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
2 | 1 | cbvdisjv 4631 |
. . . . . 6
⊢
(Disj 𝑦
∈ ran 𝐹 𝑦 ↔ Disj 𝑤 ∈ ran 𝐹 𝑤) |
3 | 2 | notbii 310 |
. . . . 5
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 ↔ ¬ Disj 𝑤 ∈ ran 𝐹 𝑤) |
4 | | id 22 |
. . . . . . 7
⊢ (𝑤 = 𝑣 → 𝑤 = 𝑣) |
5 | 4 | ndisj2 39218 |
. . . . . 6
⊢ (¬
Disj 𝑤 ∈ ran
𝐹 𝑤 ↔ ∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
6 | 5 | biimpi 206 |
. . . . 5
⊢ (¬
Disj 𝑤 ∈ ran
𝐹 𝑤 → ∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
7 | 3, 6 | sylbi 207 |
. . . 4
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
8 | | disjrnmpt2.1 |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
9 | 8 | elrnmpt 5372 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ran 𝐹 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)) |
10 | 9 | ibi 256 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
11 | 10 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
12 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧𝐵 |
13 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
14 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
15 | 12, 13, 14 | cbvmpt 4749 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑧 ∈ 𝐴 ↦ ⦋𝑧 / 𝑥⦌𝐵) |
16 | 8, 15 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ⦋𝑧 / 𝑥⦌𝐵) |
17 | 16 | elrnmpt 5372 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran 𝐹 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
18 | 17 | ibi 256 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran 𝐹 → ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) |
19 | 18 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) |
20 | 11, 19 | jca 554 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 ∧ ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
21 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑤 = 𝐵 |
22 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑣 |
23 | 22, 13 | nfeq 2776 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝐵 |
24 | 21, 23 | reean 3106 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ↔ (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 ∧ ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
25 | 20, 24 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
26 | 25 | adantr 481 |
. . . . . . . 8
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
27 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑤 |
28 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
29 | 8, 28 | nfcxfr 2762 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐹 |
30 | 29 | nfrn 5368 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥ran
𝐹 |
31 | 27, 30 | nfel 2777 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 ∈ ran 𝐹 |
32 | 30 | nfcri 2758 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑣 ∈ ran 𝐹 |
33 | 31, 32 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) |
34 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) |
35 | 33, 34 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
36 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝐵) |
37 | 14 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = ⦋𝑧 / 𝑥⦌𝐵 → 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) |
39 | 38 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = ⦋𝑧 / 𝑥⦌𝐵 → ⦋𝑧 / 𝑥⦌𝐵 = 𝑣) |
40 | 39 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → ⦋𝑧 / 𝑥⦌𝐵 = 𝑣) |
41 | 36, 37, 40 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣) |
42 | 41 | adantll 750 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣) |
43 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 ≠ 𝑣) |
44 | 43 | neneqd 2799 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) ∧ 𝑥 = 𝑧) → ¬ 𝑤 = 𝑣) |
45 | 42, 44 | pm2.65da 600 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → ¬ 𝑥 = 𝑧) |
46 | 45 | neqned 2801 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → 𝑥 ≠ 𝑧) |
47 | 46 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → 𝑥 ≠ 𝑧) |
48 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝐵 → 𝑤 = 𝐵) |
49 | 48 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝐵 → 𝐵 = 𝑤) |
50 | 49 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → 𝐵 = 𝑤) |
51 | 39 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → ⦋𝑧 / 𝑥⦌𝐵 = 𝑣) |
52 | 50, 51 | ineq12d 3815 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝑤 ∩ 𝑣)) |
53 | | simpl 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝑤 ∩ 𝑣) ≠ ∅) |
54 | 52, 53 | eqnetrd 2861 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
55 | 54 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
56 | 47, 55 | jca 554 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
57 | 56 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
58 | 57 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → ((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
59 | 58 | reximdv 3016 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → (∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
60 | 59 | a1d 25 |
. . . . . . . . 9
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → (𝑥 ∈ 𝐴 → (∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)))) |
61 | 35, 60 | reximdai 3012 |
. . . . . . . 8
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → (∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
62 | 26, 61 | mpd 15 |
. . . . . . 7
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
63 | 62 | ex 450 |
. . . . . 6
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
64 | 63 | a1i 11 |
. . . . 5
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)))) |
65 | 64 | rexlimdvv 3037 |
. . . 4
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → (∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
66 | 7, 65 | mpd 15 |
. . 3
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
67 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑢𝐵 |
68 | | nfcsb1v 3549 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
69 | | csbeq1a 3542 |
. . . . . 6
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
70 | 67, 68, 69 | cbvdisj 4630 |
. . . . 5
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵) |
71 | 70 | notbii 310 |
. . . 4
⊢ (¬
Disj 𝑥 ∈ 𝐴 𝐵 ↔ ¬ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵) |
72 | | csbeq1a 3542 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → ⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑢⦌⦋𝑢 / 𝑥⦌𝐵) |
73 | | csbco 3543 |
. . . . . . . 8
⊢
⦋𝑧 /
𝑢⦌⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
74 | 73 | a1i 11 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → ⦋𝑧 / 𝑢⦌⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
75 | 72, 74 | eqtrd 2656 |
. . . . . 6
⊢ (𝑢 = 𝑧 → ⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
76 | 75 | ndisj2 39218 |
. . . . 5
⊢ (¬
Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
77 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
78 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑢 ≠ 𝑧 |
79 | 68, 13 | nfin 3820 |
. . . . . . . . 9
⊢
Ⅎ𝑥(⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) |
80 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥∅ |
81 | 79, 80 | nfne 2894 |
. . . . . . . 8
⊢
Ⅎ𝑥(⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅ |
82 | 78, 81 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
83 | 77, 82 | nfrex 3007 |
. . . . . 6
⊢
Ⅎ𝑥∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
84 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑢∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
85 | | neeq1 2856 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → (𝑢 ≠ 𝑧 ↔ 𝑥 ≠ 𝑧)) |
86 | | csbeq1 3536 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑥 → ⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵) |
87 | | csbid 3541 |
. . . . . . . . . . . 12
⊢
⦋𝑥 /
𝑥⦌𝐵 = 𝐵 |
88 | 87 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑥 → ⦋𝑥 / 𝑥⦌𝐵 = 𝐵) |
89 | 86, 88 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑥 → ⦋𝑢 / 𝑥⦌𝐵 = 𝐵) |
90 | 89 | ineq1d 3813 |
. . . . . . . . 9
⊢ (𝑢 = 𝑥 → (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
91 | 90 | neeq1d 2853 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → ((⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅ ↔ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
92 | 85, 91 | anbi12d 747 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → ((𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) ↔ (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
93 | 92 | rexbidv 3052 |
. . . . . 6
⊢ (𝑢 = 𝑥 → (∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) ↔ ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
94 | 83, 84, 93 | cbvrex 3168 |
. . . . 5
⊢
(∃𝑢 ∈
𝐴 ∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
95 | 76, 94 | bitri 264 |
. . . 4
⊢ (¬
Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
96 | 71, 95 | bitri 264 |
. . 3
⊢ (¬
Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
97 | 66, 96 | sylibr 224 |
. 2
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ¬ Disj 𝑥 ∈ 𝐴 𝐵) |
98 | 97 | con4i 113 |
1
⊢
(Disj 𝑥
∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦) |