Proof of Theorem neicvgbex
Step | Hyp | Ref
| Expression |
1 | | neicvgbex.h |
. . . . 5
⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) |
2 | | neicvgbex.d |
. . . . . . 7
⊢ 𝐷 = (𝑃‘𝐵) |
3 | 2 | coeq1i 5527 |
. . . . . 6
⊢ (𝐷 ∘ 𝐺) = ((𝑃‘𝐵) ∘ 𝐺) |
4 | 3 | coeq2i 5528 |
. . . . 5
⊢ (𝐹 ∘ (𝐷 ∘ 𝐺)) = (𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺)) |
5 | 1, 4 | eqtri 2802 |
. . . 4
⊢ 𝐻 = (𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺)) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐻 = (𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺))) |
7 | | neicvgbex.r |
. . 3
⊢ (𝜑 → 𝑁𝐻𝑀) |
8 | 6, 7 | breqdi 4901 |
. 2
⊢ (𝜑 → 𝑁(𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺))𝑀) |
9 | | brne0 4936 |
. 2
⊢ (𝑁(𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺))𝑀 → (𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺)) ≠ ∅) |
10 | | fvprc 6439 |
. . . . . . . . . . . . 13
⊢ (¬
𝐵 ∈ V → (𝑃‘𝐵) = ∅) |
11 | 10 | dmeqd 5571 |
. . . . . . . . . . . 12
⊢ (¬
𝐵 ∈ V → dom
(𝑃‘𝐵) = dom ∅) |
12 | | dm0 5584 |
. . . . . . . . . . . 12
⊢ dom
∅ = ∅ |
13 | 11, 12 | syl6eq 2830 |
. . . . . . . . . . 11
⊢ (¬
𝐵 ∈ V → dom
(𝑃‘𝐵) = ∅) |
14 | 13 | ineq1d 4036 |
. . . . . . . . . 10
⊢ (¬
𝐵 ∈ V → (dom
(𝑃‘𝐵) ∩ ran 𝐺) = (∅ ∩ ran 𝐺)) |
15 | | incom 4028 |
. . . . . . . . . . 11
⊢ (∅
∩ ran 𝐺) = (ran 𝐺 ∩ ∅) |
16 | | in0 4194 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∩ ∅) =
∅ |
17 | 15, 16 | eqtri 2802 |
. . . . . . . . . 10
⊢ (∅
∩ ran 𝐺) =
∅ |
18 | 14, 17 | syl6eq 2830 |
. . . . . . . . 9
⊢ (¬
𝐵 ∈ V → (dom
(𝑃‘𝐵) ∩ ran 𝐺) = ∅) |
19 | 18 | coemptyd 14127 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ V → ((𝑃‘𝐵) ∘ 𝐺) = ∅) |
20 | 19 | rneqd 5598 |
. . . . . . 7
⊢ (¬
𝐵 ∈ V → ran
((𝑃‘𝐵) ∘ 𝐺) = ran ∅) |
21 | | rn0 5623 |
. . . . . . 7
⊢ ran
∅ = ∅ |
22 | 20, 21 | syl6eq 2830 |
. . . . . 6
⊢ (¬
𝐵 ∈ V → ran
((𝑃‘𝐵) ∘ 𝐺) = ∅) |
23 | 22 | ineq2d 4037 |
. . . . 5
⊢ (¬
𝐵 ∈ V → (dom
𝐹 ∩ ran ((𝑃‘𝐵) ∘ 𝐺)) = (dom 𝐹 ∩ ∅)) |
24 | | in0 4194 |
. . . . 5
⊢ (dom
𝐹 ∩ ∅) =
∅ |
25 | 23, 24 | syl6eq 2830 |
. . . 4
⊢ (¬
𝐵 ∈ V → (dom
𝐹 ∩ ran ((𝑃‘𝐵) ∘ 𝐺)) = ∅) |
26 | 25 | coemptyd 14127 |
. . 3
⊢ (¬
𝐵 ∈ V → (𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺)) = ∅) |
27 | 26 | necon1ai 2996 |
. 2
⊢ ((𝐹 ∘ ((𝑃‘𝐵) ∘ 𝐺)) ≠ ∅ → 𝐵 ∈ V) |
28 | 8, 9, 27 | 3syl 18 |
1
⊢ (𝜑 → 𝐵 ∈ V) |