| Step | Hyp | Ref
| Expression |
| 1 | | disjdsct.3 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
| 2 | | disjdsct.1 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐴 |
| 3 | 2 | disjorsf 32593 |
. . . . . . . 8
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
| 4 | 1, 3 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
| 5 | 4 | r19.21bi 3251 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
| 6 | 5 | r19.21bi 3251 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
| 7 | | simpr3 1197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) |
| 8 | | disjdsct.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅})) |
| 9 | | eldifsni 4790 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) |
| 11 | 10 | sbimi 2074 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) → [𝑖 / 𝑥]𝐵 ≠ ∅) |
| 12 | | sban 2080 |
. . . . . . . . . . . 12
⊢ ([𝑖 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ ([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥 ∈ 𝐴)) |
| 13 | | disjdsct.0 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝜑 |
| 14 | 13 | sbf 2271 |
. . . . . . . . . . . . 13
⊢ ([𝑖 / 𝑥]𝜑 ↔ 𝜑) |
| 15 | 2 | clelsb1fw 2909 |
. . . . . . . . . . . . 13
⊢ ([𝑖 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴) |
| 16 | 14, 15 | anbi12i 628 |
. . . . . . . . . . . 12
⊢ (([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴)) |
| 17 | 12, 16 | bitri 275 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴)) |
| 18 | | sbsbc 3792 |
. . . . . . . . . . . 12
⊢ ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ [𝑖 / 𝑥]𝐵 ≠ ∅) |
| 19 | | sbcne12 4415 |
. . . . . . . . . . . 12
⊢
([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑖 / 𝑥⦌∅) |
| 20 | | csb0 4410 |
. . . . . . . . . . . . 13
⊢
⦋𝑖 /
𝑥⦌∅ =
∅ |
| 21 | 20 | neeq2i 3006 |
. . . . . . . . . . . 12
⊢
(⦋𝑖 /
𝑥⦌𝐵 ≠ ⦋𝑖 / 𝑥⦌∅ ↔
⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
| 22 | 18, 19, 21 | 3bitri 297 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
| 23 | 11, 17, 22 | 3imtr3i 291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
| 24 | 23 | 3ad2antr1 1189 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
| 25 | | disj3 4454 |
. . . . . . . . . . . . 13
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ⦋𝑖 / 𝑥⦌𝐵 = (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵)) |
| 26 | 25 | biimpi 216 |
. . . . . . . . . . . 12
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ⦋𝑖 / 𝑥⦌𝐵 = (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵)) |
| 27 | 26 | neeq1d 3000 |
. . . . . . . . . . 11
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (⦋𝑖 / 𝑥⦌𝐵 ≠ ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵) ≠ ∅)) |
| 28 | 27 | biimpa 476 |
. . . . . . . . . 10
⊢
(((⦋𝑖
/ 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∧ ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) → (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵) ≠ ∅) |
| 29 | | difn0 4367 |
. . . . . . . . . 10
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵) ≠ ∅ → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢
(((⦋𝑖
/ 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∧ ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
| 31 | 7, 24, 30 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
| 32 | 31 | 3anassrs 1361 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
| 33 | 32 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
| 34 | 33 | orim2d 969 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) |
| 35 | 6, 34 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
| 36 | 35 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
| 37 | 36 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
| 38 | | nfmpt1 5250 |
. . 3
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 39 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 40 | 13, 2, 38, 39, 8 | funcnv4mpt 32679 |
. 2
⊢ (𝜑 → (Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) |
| 41 | 37, 40 | mpbird 257 |
1
⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) |