Proof of Theorem divsfval
Step | Hyp | Ref
| Expression |
1 | | ercpbl.v |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
2 | | ercpbl.r |
. . . . . 6
⊢ (𝜑 → ∼ Er 𝑉) |
3 | 2 | ecss 8378 |
. . . . 5
⊢ (𝜑 → [𝐴] ∼ ⊆ 𝑉) |
4 | 1, 3 | ssexd 5202 |
. . . 4
⊢ (𝜑 → [𝐴] ∼ ∈
V) |
5 | | eceq1 8370 |
. . . . 5
⊢ (𝑥 = 𝐴 → [𝑥] ∼ = [𝐴] ∼ ) |
6 | | ercpbl.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) |
7 | 5, 6 | fvmptg 6785 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ [𝐴] ∼ ∈ V) →
(𝐹‘𝐴) = [𝐴] ∼ ) |
8 | 4, 7 | sylan2 596 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → (𝐹‘𝐴) = [𝐴] ∼ ) |
9 | 8 | expcom 417 |
. 2
⊢ (𝜑 → (𝐴 ∈ 𝑉 → (𝐹‘𝐴) = [𝐴] ∼ )) |
10 | 6 | dmeqi 5757 |
. . . . . . . 8
⊢ dom 𝐹 = dom (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) |
11 | 2 | ecss 8378 |
. . . . . . . . . . 11
⊢ (𝜑 → [𝑥] ∼ ⊆ 𝑉) |
12 | 1, 11 | ssexd 5202 |
. . . . . . . . . 10
⊢ (𝜑 → [𝑥] ∼ ∈
V) |
13 | 12 | ralrimivw 3098 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 [𝑥] ∼ ∈
V) |
14 | | dmmptg 6084 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑉 [𝑥] ∼ ∈ V → dom
(𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) = 𝑉) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) = 𝑉) |
16 | 10, 15 | syl5eq 2786 |
. . . . . . 7
⊢ (𝜑 → dom 𝐹 = 𝑉) |
17 | 16 | eleq2d 2819 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ 𝑉)) |
18 | 17 | notbid 321 |
. . . . 5
⊢ (𝜑 → (¬ 𝐴 ∈ dom 𝐹 ↔ ¬ 𝐴 ∈ 𝑉)) |
19 | | ndmfv 6716 |
. . . . 5
⊢ (¬
𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
20 | 18, 19 | syl6bir 257 |
. . . 4
⊢ (𝜑 → (¬ 𝐴 ∈ 𝑉 → (𝐹‘𝐴) = ∅)) |
21 | | ecdmn0 8379 |
. . . . . 6
⊢ (𝐴 ∈ dom ∼ ↔ [𝐴] ∼ ≠
∅) |
22 | | erdm 8342 |
. . . . . . . . 9
⊢ ( ∼ Er
𝑉 → dom ∼ =
𝑉) |
23 | 2, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom ∼ = 𝑉) |
24 | 23 | eleq2d 2819 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ dom ∼ ↔ 𝐴 ∈ 𝑉)) |
25 | 24 | biimpd 232 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ dom ∼ → 𝐴 ∈ 𝑉)) |
26 | 21, 25 | syl5bir 246 |
. . . . 5
⊢ (𝜑 → ([𝐴] ∼ ≠ ∅ →
𝐴 ∈ 𝑉)) |
27 | 26 | necon1bd 2953 |
. . . 4
⊢ (𝜑 → (¬ 𝐴 ∈ 𝑉 → [𝐴] ∼ =
∅)) |
28 | 20, 27 | jcad 516 |
. . 3
⊢ (𝜑 → (¬ 𝐴 ∈ 𝑉 → ((𝐹‘𝐴) = ∅ ∧ [𝐴] ∼ =
∅))) |
29 | | eqtr3 2761 |
. . 3
⊢ (((𝐹‘𝐴) = ∅ ∧ [𝐴] ∼ = ∅) →
(𝐹‘𝐴) = [𝐴] ∼ ) |
30 | 28, 29 | syl6 35 |
. 2
⊢ (𝜑 → (¬ 𝐴 ∈ 𝑉 → (𝐹‘𝐴) = [𝐴] ∼ )) |
31 | 9, 30 | pm2.61d 182 |
1
⊢ (𝜑 → (𝐹‘𝐴) = [𝐴] ∼ ) |