| Step | Hyp | Ref
| Expression |
| 1 | | disjf1.xph |
. . . . . . 7
⊢
Ⅎ𝑥𝜑 |
| 2 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 3 | 1, 2 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴) |
| 4 | | nfcsb1v 3923 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
| 5 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑉 |
| 6 | 4, 5 | nfel 2920 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉 |
| 7 | 3, 6 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉) |
| 8 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
| 9 | 8 | anbi2d 630 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴))) |
| 10 | | csbeq1a 3913 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
| 11 | 10 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑉 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉)) |
| 12 | 9, 11 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉))) |
| 13 | | disjf1.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 14 | 7, 12, 13 | chvarfv 2240 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉) |
| 15 | 14 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉) |
| 16 | | inidm 4227 |
. . . . . . . . 9
⊢
(⦋𝑦 /
𝑥⦌𝐵 ∩ ⦋𝑦 / 𝑥⦌𝐵) = ⦋𝑦 / 𝑥⦌𝐵 |
| 17 | 16 | eqcomi 2746 |
. . . . . . . 8
⊢
⦋𝑦 /
𝑥⦌𝐵 = (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑦 / 𝑥⦌𝐵) |
| 18 | 17 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → ⦋𝑦 / 𝑥⦌𝐵 = (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑦 / 𝑥⦌𝐵)) |
| 19 | | ineq2 4214 |
. . . . . . . 8
⊢
(⦋𝑦 /
𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑦 / 𝑥⦌𝐵) = (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
| 20 | 19 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑦 / 𝑥⦌𝐵) = (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
| 21 | | disjf1.dj |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
| 22 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝐵 |
| 23 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 |
| 24 | | csbeq1a 3913 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
| 25 | 22, 23, 24 | cbvdisj 5120 |
. . . . . . . . . 10
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ Disj 𝑤 ∈ 𝐴 ⦋𝑤 / 𝑥⦌𝐵) |
| 26 | 21, 25 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → Disj 𝑤 ∈ 𝐴 ⦋𝑤 / 𝑥⦌𝐵) |
| 27 | 26 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → Disj 𝑤 ∈ 𝐴 ⦋𝑤 / 𝑥⦌𝐵) |
| 28 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) |
| 29 | | neqne 2948 |
. . . . . . . . 9
⊢ (¬
𝑦 = 𝑧 → 𝑦 ≠ 𝑧) |
| 30 | 29 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → 𝑦 ≠ 𝑧) |
| 31 | | csbeq1 3902 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
| 32 | | csbeq1 3902 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 33 | 31, 32 | disji2 5127 |
. . . . . . . 8
⊢
((Disj 𝑤
∈ 𝐴
⦋𝑤 / 𝑥⦌𝐵 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 ≠ 𝑧) → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) |
| 34 | 27, 28, 30, 33 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) |
| 35 | 18, 20, 34 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → ⦋𝑦 / 𝑥⦌𝐵 = ∅) |
| 36 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∅ |
| 37 | 4, 36 | nfne 3043 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ≠ ∅ |
| 38 | 3, 37 | nfim 1896 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ≠ ∅) |
| 39 | 10 | neeq1d 3000 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐵 ≠ ∅ ↔ ⦋𝑦 / 𝑥⦌𝐵 ≠ ∅)) |
| 40 | 9, 39 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ≠ ∅))) |
| 41 | | disjf1.n0 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) |
| 42 | 38, 40, 41 | chvarfv 2240 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ≠ ∅) |
| 43 | 42 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ⦋𝑦 / 𝑥⦌𝐵 ≠ ∅) |
| 44 | 43 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → ⦋𝑦 / 𝑥⦌𝐵 ≠ ∅) |
| 45 | 44 | neneqd 2945 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ∧ ¬ 𝑦 = 𝑧) → ¬ ⦋𝑦 / 𝑥⦌𝐵 = ∅) |
| 46 | 35, 45 | condan 818 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) → 𝑦 = 𝑧) |
| 47 | 46 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 → 𝑦 = 𝑧)) |
| 48 | 47 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 → 𝑦 = 𝑧)) |
| 49 | 15, 48 | jca 511 |
. 2
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 → 𝑦 = 𝑧))) |
| 50 | | disjf1.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 51 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦𝐵 |
| 52 | 51, 4, 10 | cbvmpt 5253 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
| 53 | 50, 52 | eqtri 2765 |
. . 3
⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
| 54 | | csbeq1 3902 |
. . 3
⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 55 | 53, 54 | f1mpt 7281 |
. 2
⊢ (𝐹:𝐴–1-1→𝑉 ↔ (∀𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 → 𝑦 = 𝑧))) |
| 56 | 49, 55 | sylibr 234 |
1
⊢ (𝜑 → 𝐹:𝐴–1-1→𝑉) |