Step | Hyp | Ref
| Expression |
1 | | ncaddccl 6144 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M
+c N) ∈ NC
) |
2 | | ce0nnul 6177 |
. . . . 5
⊢ ((M +c N) ∈ NC → (((M
+c N)
↑c 0c) ≠ ∅ ↔ ∃a℘1a ∈ (M +c N))) |
3 | | eladdc 4398 |
. . . . . 6
⊢ (℘1a ∈ (M +c N) ↔ ∃b ∈ M ∃g ∈ N ((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g))) |
4 | 3 | exbii 1582 |
. . . . 5
⊢ (∃a℘1a ∈ (M +c N) ↔ ∃a∃b ∈ M ∃g ∈ N ((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g))) |
5 | 2, 4 | syl6bb 252 |
. . . 4
⊢ ((M +c N) ∈ NC → (((M
+c N)
↑c 0c) ≠ ∅ ↔ ∃a∃b ∈ M ∃g ∈ N ((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g)))) |
6 | 1, 5 | syl 15 |
. . 3
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M
+c N)
↑c 0c) ≠ ∅ ↔ ∃a∃b ∈ M ∃g ∈ N ((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g)))) |
7 | | ncseqnc 6128 |
. . . . . . . 8
⊢ (M ∈ NC → (M = Nc b ↔ b ∈ M)) |
8 | | ncseqnc 6128 |
. . . . . . . 8
⊢ (N ∈ NC → (N = Nc g ↔ g ∈ N)) |
9 | 7, 8 | bi2anan9 843 |
. . . . . . 7
⊢ ((M ∈ NC ∧ N ∈ NC ) → ((M =
Nc b ∧ N = Nc g) ↔
(b ∈
M ∧
g ∈
N))) |
10 | 9 | biimpar 471 |
. . . . . 6
⊢ (((M ∈ NC ∧ N ∈ NC ) ∧ (b ∈ M ∧ g ∈ N)) → (M =
Nc b ∧ N = Nc g)) |
11 | | ssun1 3426 |
. . . . . . . . . . . 12
⊢ b ⊆ (b ∪ g) |
12 | | id 19 |
. . . . . . . . . . . 12
⊢ (℘1a = (b ∪
g) → ℘1a = (b ∪
g)) |
13 | 11, 12 | syl5sseqr 3320 |
. . . . . . . . . . 11
⊢ (℘1a = (b ∪
g) → b ⊆ ℘1a) |
14 | | ssun2 3427 |
. . . . . . . . . . . 12
⊢ g ⊆ (b ∪ g) |
15 | 14, 12 | syl5sseqr 3320 |
. . . . . . . . . . 11
⊢ (℘1a = (b ∪
g) → g ⊆ ℘1a) |
16 | 13, 15 | jca 518 |
. . . . . . . . . 10
⊢ (℘1a = (b ∪
g) → (b ⊆ ℘1a ∧ g ⊆ ℘1a)) |
17 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ b ∈
V |
18 | 17 | sspw1 4335 |
. . . . . . . . . . . 12
⊢ (b ⊆ ℘1a ↔ ∃p(p ⊆ a ∧ b = ℘1p)) |
19 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ g ∈
V |
20 | 19 | sspw1 4335 |
. . . . . . . . . . . 12
⊢ (g ⊆ ℘1a ↔ ∃q(q ⊆ a ∧ g = ℘1q)) |
21 | 18, 20 | anbi12i 678 |
. . . . . . . . . . 11
⊢ ((b ⊆ ℘1a ∧ g ⊆ ℘1a) ↔ (∃p(p ⊆ a ∧ b = ℘1p) ∧ ∃q(q ⊆ a ∧ g = ℘1q))) |
22 | | eeanv 1913 |
. . . . . . . . . . 11
⊢ (∃p∃q((p ⊆ a ∧ b = ℘1p) ∧ (q ⊆ a ∧ g = ℘1q)) ↔ (∃p(p ⊆ a ∧ b = ℘1p) ∧ ∃q(q ⊆ a ∧ g = ℘1q))) |
23 | 21, 22 | bitr4i 243 |
. . . . . . . . . 10
⊢ ((b ⊆ ℘1a ∧ g ⊆ ℘1a) ↔ ∃p∃q((p ⊆ a ∧ b = ℘1p) ∧ (q ⊆ a ∧ g = ℘1q))) |
24 | 16, 23 | sylib 188 |
. . . . . . . . 9
⊢ (℘1a = (b ∪
g) → ∃p∃q((p ⊆ a ∧ b = ℘1p) ∧ (q ⊆ a ∧ g = ℘1q))) |
25 | | pw1eq 4143 |
. . . . . . . . . . . . . . . . 17
⊢ (a = p →
℘1a = ℘1p) |
26 | 25 | eleq1d 2419 |
. . . . . . . . . . . . . . . 16
⊢ (a = p →
(℘1a ∈ Nc ℘1p ↔ ℘1p ∈ Nc ℘1p)) |
27 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
⊢ p ∈
V |
28 | 27 | pw1ex 4303 |
. . . . . . . . . . . . . . . . 17
⊢ ℘1p ∈
V |
29 | 28 | ncid 6123 |
. . . . . . . . . . . . . . . 16
⊢ ℘1p ∈ Nc ℘1p |
30 | 26, 29 | speiv 2000 |
. . . . . . . . . . . . . . 15
⊢ ∃a℘1a ∈ Nc ℘1p |
31 | | ncelncs 6120 |
. . . . . . . . . . . . . . . 16
⊢ (℘1p ∈ V → Nc ℘1p ∈ NC ) |
32 | | ce0nnul 6177 |
. . . . . . . . . . . . . . . 16
⊢ ( Nc ℘1p ∈ NC → (( Nc ℘1p ↑c 0c)
≠ ∅ ↔ ∃a℘1a ∈ Nc ℘1p)) |
33 | 28, 31, 32 | mp2b 9 |
. . . . . . . . . . . . . . 15
⊢ (( Nc ℘1p ↑c 0c)
≠ ∅ ↔ ∃a℘1a ∈ Nc ℘1p) |
34 | 30, 33 | mpbir 200 |
. . . . . . . . . . . . . 14
⊢ ( Nc ℘1p ↑c 0c)
≠ ∅ |
35 | | pw1eq 4143 |
. . . . . . . . . . . . . . . . 17
⊢ (a = q →
℘1a = ℘1q) |
36 | 35 | eleq1d 2419 |
. . . . . . . . . . . . . . . 16
⊢ (a = q →
(℘1a ∈ Nc ℘1q ↔ ℘1q ∈ Nc ℘1q)) |
37 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
⊢ q ∈
V |
38 | 37 | pw1ex 4303 |
. . . . . . . . . . . . . . . . 17
⊢ ℘1q ∈
V |
39 | 38 | ncid 6123 |
. . . . . . . . . . . . . . . 16
⊢ ℘1q ∈ Nc ℘1q |
40 | 36, 39 | speiv 2000 |
. . . . . . . . . . . . . . 15
⊢ ∃a℘1a ∈ Nc ℘1q |
41 | | ncelncs 6120 |
. . . . . . . . . . . . . . . 16
⊢ (℘1q ∈ V → Nc ℘1q ∈ NC ) |
42 | | ce0nnul 6177 |
. . . . . . . . . . . . . . . 16
⊢ ( Nc ℘1q ∈ NC → (( Nc ℘1q ↑c 0c)
≠ ∅ ↔ ∃a℘1a ∈ Nc ℘1q)) |
43 | 38, 41, 42 | mp2b 9 |
. . . . . . . . . . . . . . 15
⊢ (( Nc ℘1q ↑c 0c)
≠ ∅ ↔ ∃a℘1a ∈ Nc ℘1q) |
44 | 40, 43 | mpbir 200 |
. . . . . . . . . . . . . 14
⊢ ( Nc ℘1q ↑c 0c)
≠ ∅ |
45 | 34, 44 | pm3.2i 441 |
. . . . . . . . . . . . 13
⊢ (( Nc ℘1p ↑c 0c)
≠ ∅ ∧ (
Nc ℘1q ↑c 0c)
≠ ∅) |
46 | | nceq 6108 |
. . . . . . . . . . . . . . . 16
⊢ (b = ℘1p → Nc b = Nc ℘1p) |
47 | 46 | oveq1d 5537 |
. . . . . . . . . . . . . . 15
⊢ (b = ℘1p → ( Nc b ↑c 0c) =
( Nc ℘1p ↑c
0c)) |
48 | 47 | neeq1d 2529 |
. . . . . . . . . . . . . 14
⊢ (b = ℘1p → (( Nc b ↑c 0c)
≠ ∅ ↔ ( Nc ℘1p ↑c 0c)
≠ ∅)) |
49 | | nceq 6108 |
. . . . . . . . . . . . . . . 16
⊢ (g = ℘1q → Nc g = Nc ℘1q) |
50 | 49 | oveq1d 5537 |
. . . . . . . . . . . . . . 15
⊢ (g = ℘1q → ( Nc g ↑c 0c) =
( Nc ℘1q ↑c
0c)) |
51 | 50 | neeq1d 2529 |
. . . . . . . . . . . . . 14
⊢ (g = ℘1q → (( Nc g ↑c 0c)
≠ ∅ ↔ ( Nc ℘1q ↑c 0c)
≠ ∅)) |
52 | 48, 51 | bi2anan9 843 |
. . . . . . . . . . . . 13
⊢ ((b = ℘1p ∧ g = ℘1q) → ((( Nc
b ↑c
0c) ≠ ∅ ∧ ( Nc g ↑c 0c)
≠ ∅) ↔ (( Nc ℘1p ↑c 0c)
≠ ∅ ∧ (
Nc ℘1q ↑c 0c)
≠ ∅))) |
53 | 45, 52 | mpbiri 224 |
. . . . . . . . . . . 12
⊢ ((b = ℘1p ∧ g = ℘1q) → (( Nc
b ↑c
0c) ≠ ∅ ∧ ( Nc g ↑c 0c)
≠ ∅)) |
54 | 53 | ad2ant2l 726 |
. . . . . . . . . . 11
⊢ (((p ⊆ a ∧ b = ℘1p) ∧ (q ⊆ a ∧ g = ℘1q)) → (( Nc
b ↑c
0c) ≠ ∅ ∧ ( Nc g ↑c 0c)
≠ ∅)) |
55 | 54 | a1d 22 |
. . . . . . . . . 10
⊢ (((p ⊆ a ∧ b = ℘1p) ∧ (q ⊆ a ∧ g = ℘1q)) → ((b
∩ g) = ∅ → (( Nc
b ↑c
0c) ≠ ∅ ∧ ( Nc g ↑c 0c)
≠ ∅))) |
56 | 55 | exlimivv 1635 |
. . . . . . . . 9
⊢ (∃p∃q((p ⊆ a ∧ b = ℘1p) ∧ (q ⊆ a ∧ g = ℘1q)) → ((b
∩ g) = ∅ → (( Nc
b ↑c
0c) ≠ ∅ ∧ ( Nc g ↑c 0c)
≠ ∅))) |
57 | 24, 56 | syl 15 |
. . . . . . . 8
⊢ (℘1a = (b ∪
g) → ((b ∩ g) =
∅ → (( Nc
b ↑c
0c) ≠ ∅ ∧ ( Nc g ↑c 0c)
≠ ∅))) |
58 | 57 | impcom 419 |
. . . . . . 7
⊢ (((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g)) → (( Nc b
↑c 0c) ≠ ∅ ∧ ( Nc g
↑c 0c) ≠ ∅)) |
59 | | oveq1 5530 |
. . . . . . . . 9
⊢ (M = Nc b → (M
↑c 0c) = ( Nc b
↑c 0c)) |
60 | 59 | neeq1d 2529 |
. . . . . . . 8
⊢ (M = Nc b → ((M
↑c 0c) ≠ ∅ ↔ ( Nc
b ↑c
0c) ≠ ∅)) |
61 | | oveq1 5530 |
. . . . . . . . 9
⊢ (N = Nc g → (N
↑c 0c) = ( Nc g
↑c 0c)) |
62 | 61 | neeq1d 2529 |
. . . . . . . 8
⊢ (N = Nc g → ((N
↑c 0c) ≠ ∅ ↔ ( Nc
g ↑c
0c) ≠ ∅)) |
63 | 60, 62 | bi2anan9 843 |
. . . . . . 7
⊢ ((M = Nc b ∧ N = Nc g) → (((M
↑c 0c) ≠ ∅ ∧ (N ↑c 0c)
≠ ∅) ↔ (( Nc b
↑c 0c) ≠ ∅ ∧ ( Nc g
↑c 0c) ≠ ∅))) |
64 | 58, 63 | syl5ibr 212 |
. . . . . 6
⊢ ((M = Nc b ∧ N = Nc g) → (((b
∩ g) = ∅ ∧ ℘1a = (b ∪
g)) → ((M ↑c 0c)
≠ ∅ ∧
(N ↑c
0c) ≠ ∅))) |
65 | 10, 64 | syl 15 |
. . . . 5
⊢ (((M ∈ NC ∧ N ∈ NC ) ∧ (b ∈ M ∧ g ∈ N)) → (((b
∩ g) = ∅ ∧ ℘1a = (b ∪
g)) → ((M ↑c 0c)
≠ ∅ ∧
(N ↑c
0c) ≠ ∅))) |
66 | 65 | rexlimdvva 2745 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ NC ) → (∃b ∈ M ∃g ∈ N ((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g)) → ((M ↑c 0c)
≠ ∅ ∧
(N ↑c
0c) ≠ ∅))) |
67 | 66 | exlimdv 1636 |
. . 3
⊢ ((M ∈ NC ∧ N ∈ NC ) → (∃a∃b ∈ M ∃g ∈ N ((b ∩ g) =
∅ ∧ ℘1a = (b ∪
g)) → ((M ↑c 0c)
≠ ∅ ∧
(N ↑c
0c) ≠ ∅))) |
68 | 6, 67 | sylbid 206 |
. 2
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M
+c N)
↑c 0c) ≠ ∅ → ((M
↑c 0c) ≠ ∅ ∧ (N ↑c 0c)
≠ ∅))) |
69 | | ce0nnul 6177 |
. . . . 5
⊢ (M ∈ NC → ((M
↑c 0c) ≠ ∅ ↔ ∃b℘1b ∈ M)) |
70 | | ce0nnul 6177 |
. . . . 5
⊢ (N ∈ NC → ((N
↑c 0c) ≠ ∅ ↔ ∃g℘1g ∈ N)) |
71 | 69, 70 | bi2anan9 843 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M
↑c 0c) ≠ ∅ ∧ (N ↑c 0c)
≠ ∅) ↔ (∃b℘1b ∈ M ∧ ∃g℘1g ∈ N))) |
72 | | eeanv 1913 |
. . . 4
⊢ (∃b∃g(℘1b ∈ M ∧ ℘1g ∈ N) ↔ (∃b℘1b ∈ M ∧ ∃g℘1g ∈ N)) |
73 | 71, 72 | syl6bbr 254 |
. . 3
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M
↑c 0c) ≠ ∅ ∧ (N ↑c 0c)
≠ ∅) ↔ ∃b∃g(℘1b ∈ M ∧ ℘1g ∈ N))) |
74 | | ncseqnc 6128 |
. . . . . 6
⊢ (M ∈ NC → (M = Nc ℘1b ↔ ℘1b ∈ M)) |
75 | | ncseqnc 6128 |
. . . . . 6
⊢ (N ∈ NC → (N = Nc ℘1g ↔ ℘1g ∈ N)) |
76 | 74, 75 | bi2anan9 843 |
. . . . 5
⊢ ((M ∈ NC ∧ N ∈ NC ) → ((M =
Nc ℘1b ∧ N = Nc ℘1g) ↔ (℘1b ∈ M ∧ ℘1g ∈ N))) |
77 | | vvex 4109 |
. . . . . . . . . . . 12
⊢ V ∈ V |
78 | 17, 77 | xpsnen 6049 |
. . . . . . . . . . 11
⊢ (b × {V}) ≈ b |
79 | | enpw1 6062 |
. . . . . . . . . . 11
⊢ ((b × {V}) ≈ b ↔ ℘1(b × {V}) ≈ ℘1b) |
80 | 78, 79 | mpbi 199 |
. . . . . . . . . 10
⊢ ℘1(b × {V}) ≈ ℘1b |
81 | | snex 4111 |
. . . . . . . . . . . . 13
⊢ {V} ∈ V |
82 | 17, 81 | xpex 5115 |
. . . . . . . . . . . 12
⊢ (b × {V}) ∈
V |
83 | 82 | pw1ex 4303 |
. . . . . . . . . . 11
⊢ ℘1(b × {V}) ∈
V |
84 | 83 | eqnc 6127 |
. . . . . . . . . 10
⊢ ( Nc ℘1(b × {V}) = Nc
℘1b ↔ ℘1(b × {V}) ≈ ℘1b) |
85 | 80, 84 | mpbir 200 |
. . . . . . . . 9
⊢ Nc ℘1(b × {V}) = Nc
℘1b |
86 | | 0ex 4110 |
. . . . . . . . . . . 12
⊢ ∅ ∈
V |
87 | 19, 86 | xpsnen 6049 |
. . . . . . . . . . 11
⊢ (g × {∅})
≈ g |
88 | | enpw1 6062 |
. . . . . . . . . . 11
⊢ ((g × {∅})
≈ g ↔ ℘1(g × {∅})
≈ ℘1g) |
89 | 87, 88 | mpbi 199 |
. . . . . . . . . 10
⊢ ℘1(g × {∅})
≈ ℘1g |
90 | | snex 4111 |
. . . . . . . . . . . . 13
⊢ {∅} ∈
V |
91 | 19, 90 | xpex 5115 |
. . . . . . . . . . . 12
⊢ (g × {∅})
∈ V |
92 | 91 | pw1ex 4303 |
. . . . . . . . . . 11
⊢ ℘1(g × {∅})
∈ V |
93 | 92 | eqnc 6127 |
. . . . . . . . . 10
⊢ ( Nc ℘1(g × {∅}) =
Nc ℘1g ↔ ℘1(g × {∅})
≈ ℘1g) |
94 | 89, 93 | mpbir 200 |
. . . . . . . . 9
⊢ Nc ℘1(g × {∅}) =
Nc ℘1g |
95 | 85, 94 | addceq12i 4388 |
. . . . . . . 8
⊢ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅})) =
( Nc ℘1b +c Nc ℘1g) |
96 | 95 | oveq1i 5533 |
. . . . . . 7
⊢ (( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
↑c 0c) = (( Nc ℘1b +c Nc ℘1g) ↑c
0c) |
97 | | pw1un 4163 |
. . . . . . . . . 10
⊢ ℘1((b × {V}) ∪ (g × {∅})) =
(℘1(b × {V}) ∪ ℘1(g × {∅})) |
98 | 83 | ncid 6123 |
. . . . . . . . . . 11
⊢ ℘1(b × {V}) ∈
Nc ℘1(b × {V}) |
99 | 92 | ncid 6123 |
. . . . . . . . . . 11
⊢ ℘1(g × {∅})
∈ Nc ℘1(g × {∅}) |
100 | | vn0 3557 |
. . . . . . . . . . . . . 14
⊢ V ≠ ∅ |
101 | 77, 100 | xpnedisj 5513 |
. . . . . . . . . . . . 13
⊢ ((b × {V}) ∩ (g × {∅})) =
∅ |
102 | | pw1eq 4143 |
. . . . . . . . . . . . 13
⊢ (((b × {V}) ∩ (g × {∅})) =
∅ → ℘1((b × {V}) ∩ (g × {∅})) =
℘1∅) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ℘1((b × {V}) ∩ (g × {∅})) =
℘1∅ |
104 | | pw1in 4164 |
. . . . . . . . . . . 12
⊢ ℘1((b × {V}) ∩ (g × {∅})) =
(℘1(b × {V}) ∩ ℘1(g × {∅})) |
105 | | pw10 4161 |
. . . . . . . . . . . 12
⊢ ℘1∅
= ∅ |
106 | 103, 104,
105 | 3eqtr3i 2381 |
. . . . . . . . . . 11
⊢ (℘1(b × {V}) ∩ ℘1(g × {∅})) =
∅ |
107 | | eladdci 4399 |
. . . . . . . . . . 11
⊢ ((℘1(b × {V}) ∈
Nc ℘1(b × {V}) ∧
℘1(g × {∅})
∈ Nc ℘1(g × {∅})
∧ (℘1(b × {V}) ∩ ℘1(g × {∅})) =
∅) → (℘1(b × {V}) ∪ ℘1(g × {∅}))
∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))) |
108 | 98, 99, 106, 107 | mp3an 1277 |
. . . . . . . . . 10
⊢ (℘1(b × {V}) ∪ ℘1(g × {∅}))
∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅})) |
109 | 97, 108 | eqeltri 2423 |
. . . . . . . . 9
⊢ ℘1((b × {V}) ∪ (g × {∅}))
∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅})) |
110 | 82, 91 | unex 4106 |
. . . . . . . . . 10
⊢ ((b × {V}) ∪ (g × {∅}))
∈ V |
111 | | pw1eq 4143 |
. . . . . . . . . . 11
⊢ (a = ((b ×
{V}) ∪ (g × {∅})) → ℘1a = ℘1((b × {V}) ∪ (g × {∅}))) |
112 | 111 | eleq1d 2419 |
. . . . . . . . . 10
⊢ (a = ((b ×
{V}) ∪ (g × {∅})) → (℘1a ∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
↔ ℘1((b × {V}) ∪ (g × {∅}))
∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅})))) |
113 | 110, 112 | spcev 2946 |
. . . . . . . . 9
⊢ (℘1((b × {V}) ∪ (g × {∅}))
∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
→ ∃a℘1a ∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))) |
114 | 109, 113 | ax-mp 5 |
. . . . . . . 8
⊢ ∃a℘1a ∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅})) |
115 | 83 | ncelncsi 6121 |
. . . . . . . . . 10
⊢ Nc ℘1(b × {V}) ∈
NC |
116 | 92 | ncelncsi 6121 |
. . . . . . . . . 10
⊢ Nc ℘1(g × {∅})
∈ NC |
117 | | ncaddccl 6144 |
. . . . . . . . . 10
⊢ (( Nc ℘1(b × {V}) ∈
NC ∧ Nc ℘1(g × {∅})
∈ NC ) → (
Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
∈ NC
) |
118 | 115, 116,
117 | mp2an 653 |
. . . . . . . . 9
⊢ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
∈ NC |
119 | | ce0nnul 6177 |
. . . . . . . . 9
⊢ (( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
∈ NC → (((
Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
↑c 0c) ≠ ∅ ↔ ∃a℘1a ∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅})))) |
120 | 118, 119 | ax-mp 5 |
. . . . . . . 8
⊢ ((( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
↑c 0c) ≠ ∅ ↔ ∃a℘1a ∈ ( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))) |
121 | 114, 120 | mpbir 200 |
. . . . . . 7
⊢ (( Nc ℘1(b × {V}) +c Nc ℘1(g × {∅}))
↑c 0c) ≠ ∅ |
122 | 96, 121 | eqnetrri 2535 |
. . . . . 6
⊢ (( Nc ℘1b +c Nc ℘1g) ↑c 0c)
≠ ∅ |
123 | | addceq12 4385 |
. . . . . . . 8
⊢ ((M = Nc ℘1b ∧ N = Nc ℘1g) → (M
+c N) = ( Nc ℘1b +c Nc ℘1g)) |
124 | 123 | oveq1d 5537 |
. . . . . . 7
⊢ ((M = Nc ℘1b ∧ N = Nc ℘1g) → ((M
+c N)
↑c 0c) = (( Nc ℘1b +c Nc ℘1g) ↑c
0c)) |
125 | 124 | neeq1d 2529 |
. . . . . 6
⊢ ((M = Nc ℘1b ∧ N = Nc ℘1g) → (((M
+c N)
↑c 0c) ≠ ∅ ↔ (( Nc ℘1b +c Nc ℘1g) ↑c 0c)
≠ ∅)) |
126 | 122, 125 | mpbiri 224 |
. . . . 5
⊢ ((M = Nc ℘1b ∧ N = Nc ℘1g) → ((M
+c N)
↑c 0c) ≠ ∅) |
127 | 76, 126 | syl6bir 220 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ NC ) → ((℘1b ∈ M ∧ ℘1g ∈ N) → ((M
+c N)
↑c 0c) ≠ ∅)) |
128 | 127 | exlimdvv 1637 |
. . 3
⊢ ((M ∈ NC ∧ N ∈ NC ) → (∃b∃g(℘1b ∈ M ∧ ℘1g ∈ N) → ((M
+c N)
↑c 0c) ≠ ∅)) |
129 | 73, 128 | sylbid 206 |
. 2
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M
↑c 0c) ≠ ∅ ∧ (N ↑c 0c)
≠ ∅) → ((M +c N) ↑c 0c)
≠ ∅)) |
130 | 68, 129 | impbid 183 |
1
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M
+c N)
↑c 0c) ≠ ∅ ↔ ((M
↑c 0c) ≠ ∅ ∧ (N ↑c 0c)
≠ ∅))) |