Step | Hyp | Ref
| Expression |
1 | | fnce 6176 |
. 2
⊢
↑c Fn ( NC × NC ) |
2 | | df-ne 2518 |
. . . . . . 7
⊢ ((n ↑c m) ≠ ∅ ↔
¬ (n ↑c m) = ∅) |
3 | | n0 3559 |
. . . . . . . . 9
⊢ ((n ↑c m) ≠ ∅ ↔
∃p
p ∈
(n ↑c m)) |
4 | | elce 6175 |
. . . . . . . . . . 11
⊢ ((n ∈ NC ∧ m ∈ NC ) → (p ∈ (n
↑c m) ↔ ∃x∃y(℘1x ∈ n ∧ ℘1y ∈ m ∧ p ≈ (x
↑m y)))) |
5 | | 3simpa 952 |
. . . . . . . . . . . . 13
⊢ ((℘1x ∈ n ∧ ℘1y ∈ m ∧ p ≈ (x
↑m y)) → (℘1x ∈ n ∧ ℘1y ∈ m)) |
6 | | ce0nnuli 6178 |
. . . . . . . . . . . . . . 15
⊢ ((n ∈ NC ∧ ℘1x ∈ n) → (n
↑c 0c) ≠ ∅) |
7 | 6 | ex 423 |
. . . . . . . . . . . . . 14
⊢ (n ∈ NC → (℘1x ∈ n → (n
↑c 0c) ≠ ∅)) |
8 | | ce0nnuli 6178 |
. . . . . . . . . . . . . . 15
⊢ ((m ∈ NC ∧ ℘1y ∈ m) → (m
↑c 0c) ≠ ∅) |
9 | 8 | ex 423 |
. . . . . . . . . . . . . 14
⊢ (m ∈ NC → (℘1y ∈ m → (m
↑c 0c) ≠ ∅)) |
10 | 7, 9 | im2anan9 808 |
. . . . . . . . . . . . 13
⊢ ((n ∈ NC ∧ m ∈ NC ) → ((℘1x ∈ n ∧ ℘1y ∈ m) → ((n
↑c 0c) ≠ ∅ ∧ (m ↑c 0c)
≠ ∅))) |
11 | 5, 10 | syl5 28 |
. . . . . . . . . . . 12
⊢ ((n ∈ NC ∧ m ∈ NC ) → ((℘1x ∈ n ∧ ℘1y ∈ m ∧ p ≈ (x
↑m y)) →
((n ↑c
0c) ≠ ∅ ∧ (m
↑c 0c) ≠ ∅))) |
12 | 11 | exlimdvv 1637 |
. . . . . . . . . . 11
⊢ ((n ∈ NC ∧ m ∈ NC ) → (∃x∃y(℘1x ∈ n ∧ ℘1y ∈ m ∧ p ≈ (x
↑m y)) →
((n ↑c
0c) ≠ ∅ ∧ (m
↑c 0c) ≠ ∅))) |
13 | 4, 12 | sylbid 206 |
. . . . . . . . . 10
⊢ ((n ∈ NC ∧ m ∈ NC ) → (p ∈ (n
↑c m) →
((n ↑c
0c) ≠ ∅ ∧ (m
↑c 0c) ≠ ∅))) |
14 | 13 | exlimdv 1636 |
. . . . . . . . 9
⊢ ((n ∈ NC ∧ m ∈ NC ) → (∃p p ∈ (n ↑c m) → ((n
↑c 0c) ≠ ∅ ∧ (m ↑c 0c)
≠ ∅))) |
15 | 3, 14 | syl5bi 208 |
. . . . . . . 8
⊢ ((n ∈ NC ∧ m ∈ NC ) → ((n
↑c m) ≠ ∅ → ((n
↑c 0c) ≠ ∅ ∧ (m ↑c 0c)
≠ ∅))) |
16 | | ceclb 6183 |
. . . . . . . 8
⊢ ((n ∈ NC ∧ m ∈ NC ) → (((n
↑c 0c) ≠ ∅ ∧ (m ↑c 0c)
≠ ∅) ↔ (n ↑c m) ∈ NC )) |
17 | 15, 16 | sylibd 205 |
. . . . . . 7
⊢ ((n ∈ NC ∧ m ∈ NC ) → ((n
↑c m) ≠ ∅ → (n
↑c m) ∈ NC
)) |
18 | 2, 17 | syl5bir 209 |
. . . . . 6
⊢ ((n ∈ NC ∧ m ∈ NC ) → (¬ (n ↑c m) = ∅ →
(n ↑c m) ∈ NC )) |
19 | | elun 3220 |
. . . . . . 7
⊢ ((n ↑c m) ∈ ( NC ∪ {∅}) ↔
((n ↑c m) ∈ NC ∨ (n ↑c m) ∈ {∅})) |
20 | | ovex 5551 |
. . . . . . . . . 10
⊢ (n ↑c m) ∈
V |
21 | 20 | elsnc 3756 |
. . . . . . . . 9
⊢ ((n ↑c m) ∈ {∅} ↔ (n
↑c m) = ∅) |
22 | 21 | orbi2i 505 |
. . . . . . . 8
⊢ (((n ↑c m) ∈ NC ∨ (n ↑c m) ∈ {∅}) ↔ ((n
↑c m) ∈ NC ∨ (n
↑c m) = ∅)) |
23 | | orcom 376 |
. . . . . . . . 9
⊢ (((n ↑c m) ∈ NC ∨ (n ↑c m) = ∅) ↔
((n ↑c m) = ∅ ∨ (n
↑c m) ∈ NC
)) |
24 | | df-or 359 |
. . . . . . . . 9
⊢ (((n ↑c m) = ∅ ∨ (n
↑c m) ∈ NC ) ↔ (¬
(n ↑c m) = ∅ →
(n ↑c m) ∈ NC )) |
25 | 23, 24 | bitri 240 |
. . . . . . . 8
⊢ (((n ↑c m) ∈ NC ∨ (n ↑c m) = ∅) ↔
(¬ (n ↑c
m) = ∅
→ (n ↑c
m) ∈
NC )) |
26 | 22, 25 | bitri 240 |
. . . . . . 7
⊢ (((n ↑c m) ∈ NC ∨ (n ↑c m) ∈ {∅}) ↔ (¬ (n ↑c m) = ∅ →
(n ↑c m) ∈ NC )) |
27 | 19, 26 | bitri 240 |
. . . . . 6
⊢ ((n ↑c m) ∈ ( NC ∪ {∅}) ↔
(¬ (n ↑c
m) = ∅
→ (n ↑c
m) ∈
NC )) |
28 | 18, 27 | sylibr 203 |
. . . . 5
⊢ ((n ∈ NC ∧ m ∈ NC ) → (n
↑c m) ∈ ( NC ∪ {∅})) |
29 | 28 | rgen2a 2680 |
. . . 4
⊢ ∀n ∈ NC ∀m ∈ NC (n ↑c m) ∈ ( NC ∪ {∅}) |
30 | | fveq2 5328 |
. . . . . . 7
⊢ (p = 〈n, m〉 → ( ↑c
‘p) = ( ↑c
‘〈n, m〉)) |
31 | | df-ov 5526 |
. . . . . . 7
⊢ (n ↑c m) = ( ↑c ‘〈n, m〉) |
32 | 30, 31 | syl6eqr 2403 |
. . . . . 6
⊢ (p = 〈n, m〉 → ( ↑c
‘p) = (n ↑c m)) |
33 | 32 | eleq1d 2419 |
. . . . 5
⊢ (p = 〈n, m〉 → (( ↑c
‘p) ∈ ( NC ∪ {∅}) ↔ (n
↑c m) ∈ ( NC ∪ {∅}))) |
34 | 33 | ralxp 4825 |
. . . 4
⊢ (∀p ∈ ( NC × NC )( ↑c ‘p) ∈ ( NC ∪ {∅}) ↔
∀n
∈ NC ∀m ∈ NC (n ↑c m) ∈ ( NC ∪ {∅})) |
35 | 29, 34 | mpbir 200 |
. . 3
⊢ ∀p ∈ ( NC × NC )( ↑c ‘p) ∈ ( NC ∪ {∅}) |
36 | | fnfvrnss 5429 |
. . 3
⊢ ((
↑c Fn ( NC × NC ) ∧ ∀p ∈ ( NC × NC )( ↑c ‘p) ∈ ( NC ∪ {∅})) →
ran ↑c ⊆ ( NC ∪ {∅})) |
37 | 1, 35, 36 | mp2an 653 |
. 2
⊢ ran
↑c ⊆ ( NC ∪ {∅}) |
38 | | df-f 4791 |
. 2
⊢ (
↑c :( NC × NC )–→( NC ∪
{∅}) ↔ ( ↑c Fn (
NC × NC ) ∧ ran ↑c ⊆ ( NC ∪ {∅}))) |
39 | 1, 37, 38 | mpbir2an 886 |
1
⊢
↑c :( NC × NC )–→( NC ∪
{∅}) |