Step | Hyp | Ref
| Expression |
1 | | disjdsct.3 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
2 | | disjdsct.1 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐴 |
3 | 2 | disjorsf 29393 |
. . . . . . . 8
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
4 | 1, 3 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
5 | 4 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
6 | 5 | r19.21bi 2932 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
7 | | simpr3 1069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) |
8 | | disjdsct.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅})) |
9 | | eldifsni 4320 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) |
11 | 10 | sbimi 1886 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) → [𝑖 / 𝑥]𝐵 ≠ ∅) |
12 | | sban 2399 |
. . . . . . . . . . . 12
⊢ ([𝑖 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ ([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥 ∈ 𝐴)) |
13 | | disjdsct.0 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝜑 |
14 | 13 | sbf 2380 |
. . . . . . . . . . . . 13
⊢ ([𝑖 / 𝑥]𝜑 ↔ 𝜑) |
15 | 2 | clelsb3f 2768 |
. . . . . . . . . . . . 13
⊢ ([𝑖 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴) |
16 | 14, 15 | anbi12i 733 |
. . . . . . . . . . . 12
⊢ (([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴)) |
17 | 12, 16 | bitri 264 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴)) |
18 | | sbsbc 3439 |
. . . . . . . . . . . 12
⊢ ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ [𝑖 / 𝑥]𝐵 ≠ ∅) |
19 | | sbcne12 3986 |
. . . . . . . . . . . 12
⊢
([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑖 / 𝑥⦌∅) |
20 | | csb0 3982 |
. . . . . . . . . . . . 13
⊢
⦋𝑖 /
𝑥⦌∅ =
∅ |
21 | 20 | neeq2i 2859 |
. . . . . . . . . . . 12
⊢
(⦋𝑖 /
𝑥⦌𝐵 ≠ ⦋𝑖 / 𝑥⦌∅ ↔
⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
22 | 18, 19, 21 | 3bitri 286 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
23 | 11, 17, 22 | 3imtr3i 280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
24 | 23 | 3ad2antr1 1226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) |
25 | | disj3 4021 |
. . . . . . . . . . . . 13
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ⦋𝑖 / 𝑥⦌𝐵 = (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵)) |
26 | 25 | biimpi 206 |
. . . . . . . . . . . 12
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ⦋𝑖 / 𝑥⦌𝐵 = (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵)) |
27 | 26 | neeq1d 2853 |
. . . . . . . . . . 11
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (⦋𝑖 / 𝑥⦌𝐵 ≠ ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵) ≠ ∅)) |
28 | 27 | biimpa 501 |
. . . . . . . . . 10
⊢
(((⦋𝑖
/ 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∧ ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) → (⦋𝑖 / 𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵) ≠ ∅) |
29 | | difn0 3943 |
. . . . . . . . . 10
⊢
((⦋𝑖 /
𝑥⦌𝐵 ∖ ⦋𝑗 / 𝑥⦌𝐵) ≠ ∅ → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢
(((⦋𝑖
/ 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∧ ⦋𝑖 / 𝑥⦌𝐵 ≠ ∅) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
31 | 7, 24, 30 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
32 | 31 | 3anassrs 1290 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) ∧ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵) |
33 | 32 | ex 450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
34 | 33 | orim2d 885 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) |
35 | 6, 34 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
36 | 35 | ralrimiva 2966 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
37 | 36 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)) |
38 | | nfmpt1 4747 |
. . 3
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
39 | | eqid 2622 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
40 | 13, 2, 38, 39, 8 | funcnv4mpt 29470 |
. 2
⊢ (𝜑 → (Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) |
41 | 37, 40 | mpbird 247 |
1
⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) |