Proof of Theorem cusgrasizeindslem1
Step | Hyp | Ref
| Expression |
1 | | cusgrares.f |
. . . . 5
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
2 | 1 | dmeqi 5247 |
. . . 4
⊢ dom 𝐹 = dom (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
3 | | incom 3767 |
. . . . 5
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∩ dom 𝐸) = (dom 𝐸 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
4 | | dmres 5339 |
. . . . 5
⊢ dom
(𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) = ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∩ dom 𝐸) |
5 | | ssid 3587 |
. . . . . 6
⊢ dom 𝐸 ⊆ dom 𝐸 |
6 | | dfrab3ss 3864 |
. . . . . 6
⊢ (dom
𝐸 ⊆ dom 𝐸 → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} = (dom 𝐸 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} = (dom 𝐸 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
8 | 3, 4, 7 | 3eqtr4i 2642 |
. . . 4
⊢ dom
(𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} |
9 | 2, 8 | eqtri 2632 |
. . 3
⊢ dom 𝐹 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} |
10 | 9 | ineq1i 3772 |
. 2
⊢ (dom
𝐹 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) |
11 | | inrab 3858 |
. . 3
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = {𝑥 ∈ dom 𝐸 ∣ (𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥))} |
12 | | exmid 430 |
. . . . . . 7
⊢ (𝑁 ∈ (𝐸‘𝑥) ∨ ¬ 𝑁 ∈ (𝐸‘𝑥)) |
13 | | nnel 2892 |
. . . . . . . 8
⊢ (¬
𝑁 ∉ (𝐸‘𝑥) ↔ 𝑁 ∈ (𝐸‘𝑥)) |
14 | 13 | orbi1i 541 |
. . . . . . 7
⊢ ((¬
𝑁 ∉ (𝐸‘𝑥) ∨ ¬ 𝑁 ∈ (𝐸‘𝑥)) ↔ (𝑁 ∈ (𝐸‘𝑥) ∨ ¬ 𝑁 ∈ (𝐸‘𝑥))) |
15 | 12, 14 | mpbir 220 |
. . . . . 6
⊢ (¬
𝑁 ∉ (𝐸‘𝑥) ∨ ¬ 𝑁 ∈ (𝐸‘𝑥)) |
16 | | ianor 508 |
. . . . . 6
⊢ (¬
(𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥)) ↔ (¬ 𝑁 ∉ (𝐸‘𝑥) ∨ ¬ 𝑁 ∈ (𝐸‘𝑥))) |
17 | 15, 16 | mpbir 220 |
. . . . 5
⊢ ¬
(𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥)) |
18 | 17 | rgenw 2908 |
. . . 4
⊢
∀𝑥 ∈ dom
𝐸 ¬ (𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥)) |
19 | | rabeq0 3911 |
. . . 4
⊢ ({𝑥 ∈ dom 𝐸 ∣ (𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥))} = ∅ ↔ ∀𝑥 ∈ dom 𝐸 ¬ (𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥))) |
20 | 18, 19 | mpbir 220 |
. . 3
⊢ {𝑥 ∈ dom 𝐸 ∣ (𝑁 ∉ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑥))} = ∅ |
21 | 11, 20 | eqtri 2632 |
. 2
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ∅ |
22 | 10, 21 | eqtri 2632 |
1
⊢ (dom
𝐹 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ∅ |