Step | Hyp | Ref
| Expression |
1 | | unab 3521 |
. . 3
⊢ ({m ∣ ¬
n ∈ Nn } ∪ {m ∣ (m = ∅ ∨
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin ))}) = {m ∣ (¬
n ∈ Nn ∨ (m = ∅ ∨ (⟪m,
n⟫ ∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )))} |
2 | | df-sn 3741 |
. . . . . 6
⊢ {∅} = {m ∣ m = ∅} |
3 | | elun 3220 |
. . . . . . . . . 10
⊢ (m ∈ ((◡k <fin
“k {n}) ∪
{n}) ↔ (m ∈ (◡k <fin
“k {n}) ∨ m ∈ {n})) |
4 | | vex 2862 |
. . . . . . . . . . . . . 14
⊢ m ∈
V |
5 | 4 | elimak 4259 |
. . . . . . . . . . . . 13
⊢ (m ∈ (◡k <fin
“k {n}) ↔
∃t ∈ {n}⟪t,
m⟫ ∈ ◡k <fin
) |
6 | | vex 2862 |
. . . . . . . . . . . . . 14
⊢ n ∈
V |
7 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
⊢ (t = n →
⟪t, m⟫ = ⟪n, m⟫) |
8 | 7 | eleq1d 2419 |
. . . . . . . . . . . . . 14
⊢ (t = n →
(⟪t, m⟫ ∈ ◡k <fin
↔ ⟪n, m⟫ ∈ ◡k <fin
)) |
9 | 6, 8 | rexsn 3768 |
. . . . . . . . . . . . 13
⊢ (∃t ∈ {n}⟪t,
m⟫ ∈ ◡k <fin
↔ ⟪n, m⟫ ∈ ◡k <fin
) |
10 | 5, 9 | bitri 240 |
. . . . . . . . . . . 12
⊢ (m ∈ (◡k <fin
“k {n}) ↔
⟪n, m⟫ ∈ ◡k <fin
) |
11 | 6, 4 | opkelcnvk 4250 |
. . . . . . . . . . . 12
⊢ (⟪n, m⟫
∈ ◡k <fin
↔ ⟪m, n⟫ ∈
<fin ) |
12 | 10, 11 | bitri 240 |
. . . . . . . . . . 11
⊢ (m ∈ (◡k <fin
“k {n}) ↔
⟪m, n⟫ ∈
<fin ) |
13 | 4 | elsnc 3756 |
. . . . . . . . . . 11
⊢ (m ∈ {n} ↔ m =
n) |
14 | 12, 13 | orbi12i 507 |
. . . . . . . . . 10
⊢ ((m ∈ (◡k <fin
“k {n}) ∨ m ∈ {n}) ↔
(⟪m, n⟫ ∈
<fin ∨ m = n)) |
15 | 3, 14 | bitri 240 |
. . . . . . . . 9
⊢ (m ∈ ((◡k <fin
“k {n}) ∪
{n}) ↔ (⟪m, n⟫
∈ <fin
∨ m = n)) |
16 | 4 | elimak 4259 |
. . . . . . . . . 10
⊢ (m ∈ (
<fin “k {n}) ↔ ∃t ∈ {n}⟪t,
m⟫ ∈ <fin ) |
17 | 7 | eleq1d 2419 |
. . . . . . . . . . 11
⊢ (t = n →
(⟪t, m⟫ ∈
<fin ↔ ⟪n,
m⟫ ∈ <fin )) |
18 | 6, 17 | rexsn 3768 |
. . . . . . . . . 10
⊢ (∃t ∈ {n}⟪t,
m⟫ ∈ <fin ↔ ⟪n, m⟫
∈ <fin ) |
19 | 16, 18 | bitri 240 |
. . . . . . . . 9
⊢ (m ∈ (
<fin “k {n}) ↔ ⟪n, m⟫
∈ <fin ) |
20 | 15, 19 | orbi12i 507 |
. . . . . . . 8
⊢ ((m ∈ ((◡k <fin
“k {n}) ∪
{n}) ∨
m ∈ (
<fin “k {n})) ↔ ((⟪m, n⟫
∈ <fin
∨ m = n) ∨
⟪n, m⟫ ∈
<fin )) |
21 | | elun 3220 |
. . . . . . . 8
⊢ (m ∈ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n})) ↔
(m ∈
((◡k
<fin “k {n}) ∪ {n})
∨ m ∈ ( <fin “k
{n}))) |
22 | | df-3or 935 |
. . . . . . . 8
⊢ ((⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ) ↔ ((⟪m,
n⟫ ∈ <fin
∨ m = n) ∨
⟪n, m⟫ ∈
<fin )) |
23 | 20, 21, 22 | 3bitr4i 268 |
. . . . . . 7
⊢ (m ∈ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n})) ↔
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )) |
24 | 23 | abbi2i 2464 |
. . . . . 6
⊢ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n})) =
{m ∣
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )} |
25 | 2, 24 | uneq12i 3416 |
. . . . 5
⊢ ({∅} ∪ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n}))) =
({m ∣
m = ∅}
∪ {m ∣ (⟪m,
n⟫ ∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )}) |
26 | | unab 3521 |
. . . . 5
⊢ ({m ∣ m = ∅} ∪
{m ∣
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )}) = {m ∣ (m = ∅ ∨ (⟪m,
n⟫ ∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ))} |
27 | 25, 26 | eqtri 2373 |
. . . 4
⊢ ({∅} ∪ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n}))) =
{m ∣
(m = ∅
∨ (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ))} |
28 | 27 | uneq2i 3415 |
. . 3
⊢ ({m ∣ ¬
n ∈ Nn } ∪ ({∅} ∪
(((◡k
<fin “k {n}) ∪ {n})
∪ ( <fin “k {n})))) = ({m
∣ ¬ n ∈ Nn } ∪ {m ∣ (m = ∅ ∨
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin ))}) |
29 | | imor 401 |
. . . . 5
⊢ ((n ∈ Nn → (m ≠
∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ))) ↔ (¬ n
∈ Nn ∨ (m ≠ ∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )))) |
30 | | df-ne 2518 |
. . . . . . . 8
⊢ (m ≠ ∅ ↔
¬ m = ∅) |
31 | 30 | imbi1i 315 |
. . . . . . 7
⊢ ((m ≠ ∅ →
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )) ↔ (¬ m = ∅ →
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin ))) |
32 | | df-or 359 |
. . . . . . 7
⊢ ((m = ∅ ∨ (⟪m,
n⟫ ∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )) ↔ (¬ m =
∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ))) |
33 | 31, 32 | bitr4i 243 |
. . . . . 6
⊢ ((m ≠ ∅ →
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )) ↔ (m = ∅ ∨ (⟪m,
n⟫ ∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ))) |
34 | 33 | orbi2i 505 |
. . . . 5
⊢ ((¬ n ∈ Nn ∨ (m ≠ ∅ →
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin ))) ↔ (¬ n ∈ Nn ∨ (m = ∅ ∨ (⟪m,
n⟫ ∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )))) |
35 | 29, 34 | bitri 240 |
. . . 4
⊢ ((n ∈ Nn → (m ≠
∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin ))) ↔ (¬ n
∈ Nn ∨ (m = ∅ ∨
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )))) |
36 | 35 | abbii 2465 |
. . 3
⊢ {m ∣ (n ∈ Nn → (m ≠
∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )))} = {m ∣ (¬ n
∈ Nn ∨ (m = ∅ ∨
(⟪m, n⟫ ∈
<fin ∨ m = n ∨ ⟪n,
m⟫ ∈ <fin )))} |
37 | 1, 28, 36 | 3eqtr4i 2383 |
. 2
⊢ ({m ∣ ¬
n ∈ Nn } ∪ ({∅} ∪
(((◡k
<fin “k {n}) ∪ {n})
∪ ( <fin “k {n})))) = {m
∣ (n
∈ Nn →
(m ≠ ∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )))} |
38 | | abexv 4324 |
. . 3
⊢ {m ∣ ¬
n ∈ Nn } ∈
V |
39 | | snex 4111 |
. . . 4
⊢ {∅} ∈
V |
40 | | ltfinex 4464 |
. . . . . . . 8
⊢ <fin
∈ V |
41 | 40 | cnvkex 4287 |
. . . . . . 7
⊢ ◡k <fin ∈ V |
42 | | snex 4111 |
. . . . . . 7
⊢ {n} ∈
V |
43 | 41, 42 | imakex 4300 |
. . . . . 6
⊢ (◡k <fin
“k {n}) ∈ V |
44 | 43, 42 | unex 4106 |
. . . . 5
⊢ ((◡k <fin
“k {n}) ∪
{n}) ∈
V |
45 | 40, 42 | imakex 4300 |
. . . . 5
⊢ (
<fin “k {n}) ∈
V |
46 | 44, 45 | unex 4106 |
. . . 4
⊢ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n})) ∈ V |
47 | 39, 46 | unex 4106 |
. . 3
⊢ ({∅} ∪ (((◡k <fin
“k {n}) ∪
{n}) ∪ ( <fin
“k {n}))) ∈ V |
48 | 38, 47 | unex 4106 |
. 2
⊢ ({m ∣ ¬
n ∈ Nn } ∪ ({∅} ∪
(((◡k
<fin “k {n}) ∪ {n})
∪ ( <fin “k {n})))) ∈
V |
49 | 37, 48 | eqeltrri 2424 |
1
⊢ {m ∣ (n ∈ Nn → (m ≠
∅ → (⟪m, n⟫
∈ <fin
∨ m = n ∨
⟪n, m⟫ ∈
<fin )))} ∈ V |