| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . . 6
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
| 2 | 1 | cbvdisjv 5121 |
. . . . 5
⊢
(Disj 𝑦
∈ ran 𝐹 𝑦 ↔ Disj 𝑤 ∈ ran 𝐹 𝑤) |
| 3 | | id 22 |
. . . . . . 7
⊢ (𝑤 = 𝑣 → 𝑤 = 𝑣) |
| 4 | 3 | ndisj2 45056 |
. . . . . 6
⊢ (¬
Disj 𝑤 ∈ ran
𝐹 𝑤 ↔ ∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
| 5 | 4 | biimpi 216 |
. . . . 5
⊢ (¬
Disj 𝑤 ∈ ran
𝐹 𝑤 → ∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
| 6 | 2, 5 | sylnbi 330 |
. . . 4
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
| 7 | | disjrnmpt2.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 8 | 7 | elrnmpt 5969 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ran 𝐹 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)) |
| 9 | 8 | ibi 267 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
| 10 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧𝐵 |
| 11 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
| 12 | | csbeq1a 3913 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 13 | 10, 11, 12 | cbvmpt 5253 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑧 ∈ 𝐴 ↦ ⦋𝑧 / 𝑥⦌𝐵) |
| 14 | 7, 13 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ⦋𝑧 / 𝑥⦌𝐵) |
| 15 | 14 | elrnmpt 5969 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran 𝐹 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 16 | 15 | ibi 267 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran 𝐹 → ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) |
| 17 | 9, 16 | anim12i 613 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 ∧ ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 18 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑤 = 𝐵 |
| 19 | 11 | nfeq2 2923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝐵 |
| 20 | 18, 19 | reean 3316 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ↔ (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 ∧ ∃𝑧 ∈ 𝐴 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 21 | 17, 20 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 22 | 21 | adantr 480 |
. . . . . . . 8
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 23 | | nfmpt1 5250 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 24 | 7, 23 | nfcxfr 2903 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐹 |
| 25 | 24 | nfrn 5963 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥ran
𝐹 |
| 26 | 25 | nfcri 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 ∈ ran 𝐹 |
| 27 | 25 | nfcri 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑣 ∈ ran 𝐹 |
| 28 | 26, 27 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) |
| 29 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) |
| 30 | 28, 29 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) |
| 31 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝐵) |
| 32 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 33 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = ⦋𝑧 / 𝑥⦌𝐵 → 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = ⦋𝑧 / 𝑥⦌𝐵 → ⦋𝑧 / 𝑥⦌𝐵 = 𝑣) |
| 35 | 34 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → ⦋𝑧 / 𝑥⦌𝐵 = 𝑣) |
| 36 | 31, 32, 35 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣) |
| 37 | 36 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣) |
| 38 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 ≠ 𝑣) |
| 39 | 38 | neneqd 2945 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) ∧ 𝑥 = 𝑧) → ¬ 𝑤 = 𝑣) |
| 40 | 37, 39 | pm2.65da 817 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → ¬ 𝑥 = 𝑧) |
| 41 | 40 | neqned 2947 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ≠ 𝑣 ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → 𝑥 ≠ 𝑧) |
| 42 | 41 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → 𝑥 ≠ 𝑧) |
| 43 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝐵 → 𝑤 = 𝐵) |
| 44 | 43 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝐵 → 𝐵 = 𝑤) |
| 45 | 44 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → 𝐵 = 𝑤) |
| 46 | 34 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → ⦋𝑧 / 𝑥⦌𝐵 = 𝑣) |
| 47 | 45, 46 | ineq12d 4221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝑤 ∩ 𝑣)) |
| 48 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝑤 ∩ 𝑣) ≠ ∅) |
| 49 | 47, 48 | eqnetrd 3008 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∩ 𝑣) ≠ ∅ ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
| 50 | 49 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
| 51 | 42, 50 | jca 511 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) ∧ (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵)) → (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 52 | 51 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → ((𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 54 | 53 | reximdv 3170 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → (∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 55 | 54 | a1d 25 |
. . . . . . . . 9
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → (𝑥 ∈ 𝐴 → (∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)))) |
| 56 | 30, 55 | reximdai 3261 |
. . . . . . . 8
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → (∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑤 = 𝐵 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 57 | 22, 56 | mpd 15 |
. . . . . . 7
⊢ (((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) ∧ (𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅)) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 58 | 57 | ex 412 |
. . . . . 6
⊢ ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 59 | 58 | a1i 11 |
. . . . 5
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ((𝑤 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹) → ((𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)))) |
| 60 | 59 | rexlimdvv 3212 |
. . . 4
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → (∃𝑤 ∈ ran 𝐹∃𝑣 ∈ ran 𝐹(𝑤 ≠ 𝑣 ∧ (𝑤 ∩ 𝑣) ≠ ∅) → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 61 | 6, 60 | mpd 15 |
. . 3
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 62 | | csbeq1 3902 |
. . . . . 6
⊢ (𝑢 = 𝑧 → ⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 63 | 62 | ndisj2 45056 |
. . . . 5
⊢ (¬
Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 64 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
| 65 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑢 ≠ 𝑧 |
| 66 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
| 67 | 66, 11 | nfin 4224 |
. . . . . . . . 9
⊢
Ⅎ𝑥(⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) |
| 68 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥∅ |
| 69 | 67, 68 | nfne 3043 |
. . . . . . . 8
⊢
Ⅎ𝑥(⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅ |
| 70 | 65, 69 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
| 71 | 64, 70 | nfrexw 3313 |
. . . . . 6
⊢
Ⅎ𝑥∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
| 72 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑢∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) |
| 73 | | neeq1 3003 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → (𝑢 ≠ 𝑧 ↔ 𝑥 ≠ 𝑧)) |
| 74 | | csbeq1 3902 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑥 → ⦋𝑢 / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵) |
| 75 | | csbid 3912 |
. . . . . . . . . . 11
⊢
⦋𝑥 /
𝑥⦌𝐵 = 𝐵 |
| 76 | 74, 75 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑥 → ⦋𝑢 / 𝑥⦌𝐵 = 𝐵) |
| 77 | 76 | ineq1d 4219 |
. . . . . . . . 9
⊢ (𝑢 = 𝑥 → (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
| 78 | 77 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → ((⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅ ↔ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 79 | 73, 78 | anbi12d 632 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → ((𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) ↔ (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 80 | 79 | rexbidv 3179 |
. . . . . 6
⊢ (𝑢 = 𝑥 → (∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) ↔ ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅))) |
| 81 | 71, 72, 80 | cbvrexw 3307 |
. . . . 5
⊢
(∃𝑢 ∈
𝐴 ∃𝑧 ∈ 𝐴 (𝑢 ≠ 𝑧 ∧ (⦋𝑢 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅) ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 82 | 63, 81 | bitri 275 |
. . . 4
⊢ (¬
Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 83 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑢𝐵 |
| 84 | | csbeq1a 3913 |
. . . . 5
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
| 85 | 83, 66, 84 | cbvdisj 5120 |
. . . 4
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑥⦌𝐵) |
| 86 | 82, 85 | xchnxbir 333 |
. . 3
⊢ (¬
Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑧 ∧ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) ≠ ∅)) |
| 87 | 61, 86 | sylibr 234 |
. 2
⊢ (¬
Disj 𝑦 ∈ ran
𝐹 𝑦 → ¬ Disj 𝑥 ∈ 𝐴 𝐵) |
| 88 | 87 | con4i 114 |
1
⊢
(Disj 𝑥
∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦) |