Step | Hyp | Ref
| Expression |
1 | | evennn 4506 |
. . . . . 6
⊢ (x ∈ Evenfin → x ∈ Nn ) |
2 | | evennnul 4508 |
. . . . . 6
⊢ (x ∈ Evenfin → x ≠ ∅) |
3 | | eldifsn 3839 |
. . . . . 6
⊢ (x ∈ ( Nn ∖ {∅}) ↔ (x
∈ Nn ∧ x ≠ ∅)) |
4 | 1, 2, 3 | sylanbrc 645 |
. . . . 5
⊢ (x ∈ Evenfin → x ∈ ( Nn ∖ {∅})) |
5 | 4 | ssriv 3277 |
. . . 4
⊢ Evenfin ⊆
( Nn ∖ {∅}) |
6 | | oddnn 4507 |
. . . . . 6
⊢ (x ∈ Oddfin → x ∈ Nn ) |
7 | | oddnnul 4509 |
. . . . . 6
⊢ (x ∈ Oddfin → x ≠ ∅) |
8 | 6, 7, 3 | sylanbrc 645 |
. . . . 5
⊢ (x ∈ Oddfin → x ∈ ( Nn ∖ {∅})) |
9 | 8 | ssriv 3277 |
. . . 4
⊢ Oddfin ⊆ (
Nn ∖ {∅}) |
10 | 5, 9 | pm3.2i 441 |
. . 3
⊢ ( Evenfin ⊆
( Nn ∖ {∅}) ∧ Oddfin ⊆ (
Nn ∖ {∅})) |
11 | | unss 3437 |
. . 3
⊢ (( Evenfin ⊆
( Nn ∖ {∅}) ∧ Oddfin ⊆ (
Nn ∖ {∅})) ↔ ( Evenfin ∪ Oddfin ) ⊆
( Nn ∖ {∅})) |
12 | 10, 11 | mpbi 199 |
. 2
⊢ ( Evenfin ∪ Oddfin ) ⊆
( Nn ∖ {∅}) |
13 | | eldifsn 3839 |
. . . 4
⊢ (n ∈ ( Nn ∖ {∅}) ↔ (n
∈ Nn ∧ n ≠ ∅)) |
14 | | vex 2862 |
. . . . . . . . . . . 12
⊢ m ∈
V |
15 | 14 | elsnc 3756 |
. . . . . . . . . . 11
⊢ (m ∈ {∅} ↔ m =
∅) |
16 | | df-ne 2518 |
. . . . . . . . . . . 12
⊢ (m ≠ ∅ ↔
¬ m = ∅) |
17 | 16 | con2bii 322 |
. . . . . . . . . . 11
⊢ (m = ∅ ↔
¬ m ≠ ∅) |
18 | 15, 17 | bitri 240 |
. . . . . . . . . 10
⊢ (m ∈ {∅} ↔ ¬ m ≠ ∅) |
19 | 18 | orbi1i 506 |
. . . . . . . . 9
⊢ ((m ∈ {∅} ∨ m ∈ ( Evenfin ∪ Oddfin )) ↔ (¬ m ≠ ∅ ∨ m ∈ ( Evenfin
∪ Oddfin ))) |
20 | | elun 3220 |
. . . . . . . . 9
⊢ (m ∈ ({∅} ∪ ( Evenfin ∪ Oddfin )) ↔ (m ∈ {∅} ∨ m ∈ ( Evenfin ∪ Oddfin ))) |
21 | | imor 401 |
. . . . . . . . 9
⊢ ((m ≠ ∅ →
m ∈ (
Evenfin ∪ Oddfin )) ↔ (¬ m ≠ ∅ ∨ m ∈ ( Evenfin
∪ Oddfin ))) |
22 | 19, 20, 21 | 3bitr4i 268 |
. . . . . . . 8
⊢ (m ∈ ({∅} ∪ ( Evenfin ∪ Oddfin )) ↔ (m ≠ ∅ →
m ∈ (
Evenfin ∪ Oddfin ))) |
23 | 22 | abbi2i 2464 |
. . . . . . 7
⊢ ({∅} ∪ ( Evenfin ∪ Oddfin )) = {m ∣ (m ≠ ∅ →
m ∈ (
Evenfin ∪ Oddfin ))} |
24 | | snex 4111 |
. . . . . . . 8
⊢ {∅} ∈
V |
25 | | evenfinex 4503 |
. . . . . . . . 9
⊢ Evenfin ∈
V |
26 | | oddfinex 4504 |
. . . . . . . . 9
⊢ Oddfin ∈
V |
27 | 25, 26 | unex 4106 |
. . . . . . . 8
⊢ ( Evenfin ∪ Oddfin ) ∈
V |
28 | 24, 27 | unex 4106 |
. . . . . . 7
⊢ ({∅} ∪ ( Evenfin ∪ Oddfin )) ∈
V |
29 | 23, 28 | eqeltrri 2424 |
. . . . . 6
⊢ {m ∣ (m ≠ ∅ →
m ∈ (
Evenfin ∪ Oddfin ))} ∈ V |
30 | | neeq1 2524 |
. . . . . . 7
⊢ (m = 0c → (m ≠ ∅ ↔
0c ≠ ∅)) |
31 | | eleq1 2413 |
. . . . . . 7
⊢ (m = 0c → (m ∈ ( Evenfin ∪ Oddfin ) ↔ 0c ∈ ( Evenfin
∪ Oddfin ))) |
32 | 30, 31 | imbi12d 311 |
. . . . . 6
⊢ (m = 0c → ((m ≠ ∅ →
m ∈ (
Evenfin ∪ Oddfin )) ↔ (0c ≠
∅ → 0c ∈ ( Evenfin
∪ Oddfin )))) |
33 | | neeq1 2524 |
. . . . . . 7
⊢ (m = k →
(m ≠ ∅ ↔ k
≠ ∅)) |
34 | | eleq1 2413 |
. . . . . . 7
⊢ (m = k →
(m ∈ (
Evenfin ∪ Oddfin ) ↔ k ∈ ( Evenfin ∪ Oddfin ))) |
35 | 33, 34 | imbi12d 311 |
. . . . . 6
⊢ (m = k →
((m ≠ ∅ → m
∈ ( Evenfin ∪ Oddfin )) ↔ (k ≠ ∅ →
k ∈ (
Evenfin ∪ Oddfin )))) |
36 | | neeq1 2524 |
. . . . . . 7
⊢ (m = (k
+c 1c) → (m ≠ ∅ ↔
(k +c
1c) ≠ ∅)) |
37 | | eleq1 2413 |
. . . . . . 7
⊢ (m = (k
+c 1c) → (m ∈ ( Evenfin ∪ Oddfin ) ↔ (k +c 1c) ∈ ( Evenfin
∪ Oddfin ))) |
38 | 36, 37 | imbi12d 311 |
. . . . . 6
⊢ (m = (k
+c 1c) → ((m ≠ ∅ →
m ∈ (
Evenfin ∪ Oddfin )) ↔ ((k +c 1c) ≠
∅ → (k +c 1c) ∈ ( Evenfin
∪ Oddfin )))) |
39 | | neeq1 2524 |
. . . . . . 7
⊢ (m = n →
(m ≠ ∅ ↔ n
≠ ∅)) |
40 | | eleq1 2413 |
. . . . . . 7
⊢ (m = n →
(m ∈ (
Evenfin ∪ Oddfin ) ↔ n ∈ ( Evenfin ∪ Oddfin ))) |
41 | 39, 40 | imbi12d 311 |
. . . . . 6
⊢ (m = n →
((m ≠ ∅ → m
∈ ( Evenfin ∪ Oddfin )) ↔ (n ≠ ∅ →
n ∈ (
Evenfin ∪ Oddfin )))) |
42 | | ssun1 3426 |
. . . . . . . 8
⊢ Evenfin ⊆
( Evenfin ∪ Oddfin ) |
43 | | 0ceven 4505 |
. . . . . . . 8
⊢
0c ∈ Evenfin |
44 | 42, 43 | sselii 3270 |
. . . . . . 7
⊢
0c ∈ ( Evenfin ∪ Oddfin ) |
45 | 44 | a1i 10 |
. . . . . 6
⊢
(0c ≠ ∅ →
0c ∈ ( Evenfin ∪ Oddfin )) |
46 | | addcnnul 4453 |
. . . . . . . . . 10
⊢ ((k +c 1c) ≠
∅ → (k ≠ ∅ ∧ 1c ≠ ∅)) |
47 | 46 | simpld 445 |
. . . . . . . . 9
⊢ ((k +c 1c) ≠
∅ → k ≠ ∅) |
48 | | sucevenodd 4510 |
. . . . . . . . . . . 12
⊢ ((k ∈ Evenfin ∧
(k +c
1c) ≠ ∅) →
(k +c
1c) ∈ Oddfin ) |
49 | 48 | expcom 424 |
. . . . . . . . . . 11
⊢ ((k +c 1c) ≠
∅ → (k ∈ Evenfin → (k +c 1c) ∈ Oddfin
)) |
50 | | sucoddeven 4511 |
. . . . . . . . . . . 12
⊢ ((k ∈ Oddfin ∧
(k +c
1c) ≠ ∅) →
(k +c
1c) ∈ Evenfin ) |
51 | 50 | expcom 424 |
. . . . . . . . . . 11
⊢ ((k +c 1c) ≠
∅ → (k ∈ Oddfin → (k +c 1c) ∈ Evenfin
)) |
52 | 49, 51 | orim12d 811 |
. . . . . . . . . 10
⊢ ((k +c 1c) ≠
∅ → ((k ∈ Evenfin ∨
k ∈ Oddfin ) → ((k +c 1c) ∈ Oddfin
∨ (k
+c 1c) ∈
Evenfin ))) |
53 | | elun 3220 |
. . . . . . . . . 10
⊢ (k ∈ ( Evenfin ∪ Oddfin ) ↔ (k ∈ Evenfin ∨
k ∈ Oddfin )) |
54 | | elun 3220 |
. . . . . . . . . . 11
⊢ ((k +c 1c) ∈ ( Evenfin
∪ Oddfin ) ↔ ((k +c 1c) ∈ Evenfin
∨ (k
+c 1c) ∈
Oddfin )) |
55 | | orcom 376 |
. . . . . . . . . . 11
⊢ (((k +c 1c) ∈ Evenfin
∨ (k
+c 1c) ∈
Oddfin ) ↔ ((k +c 1c) ∈ Oddfin
∨ (k
+c 1c) ∈
Evenfin )) |
56 | 54, 55 | bitri 240 |
. . . . . . . . . 10
⊢ ((k +c 1c) ∈ ( Evenfin
∪ Oddfin ) ↔ ((k +c 1c) ∈ Oddfin
∨ (k
+c 1c) ∈
Evenfin )) |
57 | 52, 53, 56 | 3imtr4g 261 |
. . . . . . . . 9
⊢ ((k +c 1c) ≠
∅ → (k ∈ ( Evenfin ∪ Oddfin ) → (k +c 1c) ∈ ( Evenfin
∪ Oddfin ))) |
58 | 47, 57 | embantd 50 |
. . . . . . . 8
⊢ ((k +c 1c) ≠
∅ → ((k ≠ ∅ →
k ∈ (
Evenfin ∪ Oddfin )) → (k +c 1c) ∈ ( Evenfin
∪ Oddfin ))) |
59 | 58 | com12 27 |
. . . . . . 7
⊢ ((k ≠ ∅ →
k ∈ (
Evenfin ∪ Oddfin )) → ((k +c 1c) ≠
∅ → (k +c 1c) ∈ ( Evenfin
∪ Oddfin ))) |
60 | 59 | a1i 10 |
. . . . . 6
⊢ (k ∈ Nn → ((k ≠
∅ → k ∈ ( Evenfin ∪ Oddfin )) → ((k +c 1c) ≠
∅ → (k +c 1c) ∈ ( Evenfin
∪ Oddfin )))) |
61 | 29, 32, 35, 38, 41, 45, 60 | finds 4411 |
. . . . 5
⊢ (n ∈ Nn → (n ≠
∅ → n ∈ ( Evenfin ∪ Oddfin ))) |
62 | 61 | imp 418 |
. . . 4
⊢ ((n ∈ Nn ∧ n ≠ ∅) →
n ∈ (
Evenfin ∪ Oddfin )) |
63 | 13, 62 | sylbi 187 |
. . 3
⊢ (n ∈ ( Nn ∖ {∅}) → n
∈ ( Evenfin ∪ Oddfin )) |
64 | 63 | ssriv 3277 |
. 2
⊢ ( Nn ∖ {∅}) ⊆ ( Evenfin ∪ Oddfin ) |
65 | 12, 64 | eqssi 3288 |
1
⊢ ( Evenfin ∪ Oddfin ) = ( Nn
∖ {∅}) |