Step | Hyp | Ref
| Expression |
1 | | inpreima 6342 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) = ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵))) |
2 | | imaeq2 5462 |
. . . . . . . . . 10
⊢
((⦋𝑦 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → (◡𝐹 “ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) = (◡𝐹 “ ∅)) |
3 | | ima0 5481 |
. . . . . . . . . 10
⊢ (◡𝐹 “ ∅) = ∅ |
4 | 2, 3 | syl6eq 2672 |
. . . . . . . . 9
⊢
((⦋𝑦 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → (◡𝐹 “ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) = ∅) |
5 | 1, 4 | sylan9req 2677 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧
(⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) = ∅) |
6 | 5 | ex 450 |
. . . . . . 7
⊢ (Fun
𝐹 →
((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) = ∅)) |
7 | | csbima12 5483 |
. . . . . . . . . 10
⊢
⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) = (⦋𝑦 / 𝑥⦌◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) |
8 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
9 | | csbconstg 3546 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌◡𝐹 = ◡𝐹) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . 11
⊢
⦋𝑦 /
𝑥⦌◡𝐹 = ◡𝐹 |
11 | 10 | imaeq1i 5463 |
. . . . . . . . . 10
⊢
(⦋𝑦 /
𝑥⦌◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) = (◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) |
12 | 7, 11 | eqtri 2644 |
. . . . . . . . 9
⊢
⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) = (◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) |
13 | | csbima12 5483 |
. . . . . . . . . 10
⊢
⦋𝑧 /
𝑥⦌(◡𝐹 “ 𝐵) = (⦋𝑧 / 𝑥⦌◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) |
14 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
15 | | csbconstg 3546 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌◡𝐹 = ◡𝐹) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
⊢
⦋𝑧 /
𝑥⦌◡𝐹 = ◡𝐹 |
17 | 16 | imaeq1i 5463 |
. . . . . . . . . 10
⊢
(⦋𝑧 /
𝑥⦌◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) = (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) |
18 | 13, 17 | eqtri 2644 |
. . . . . . . . 9
⊢
⦋𝑧 /
𝑥⦌(◡𝐹 “ 𝐵) = (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) |
19 | 12, 18 | ineq12i 3812 |
. . . . . . . 8
⊢
(⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) |
20 | 19 | eqeq1i 2627 |
. . . . . . 7
⊢
((⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅ ↔ ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) = ∅) |
21 | 6, 20 | syl6ibr 242 |
. . . . . 6
⊢ (Fun
𝐹 →
((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅)) |
22 | 21 | orim2d 885 |
. . . . 5
⊢ (Fun
𝐹 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅))) |
23 | 22 | ralimdv 2963 |
. . . 4
⊢ (Fun
𝐹 → (∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅))) |
24 | 23 | ralimdv 2963 |
. . 3
⊢ (Fun
𝐹 → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅))) |
25 | | disjors 4635 |
. . 3
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
26 | | disjors 4635 |
. . 3
⊢
(Disj 𝑥
∈ 𝐴 (◡𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅)) |
27 | 24, 25, 26 | 3imtr4g 285 |
. 2
⊢ (Fun
𝐹 → (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))) |
28 | 27 | imp 445 |
1
⊢ ((Fun
𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) |