Description: An exponentiation law for alephs. Lemma 6.1 of Jech p. 42. (Contributed by NM, 29-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | alephexp1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alephon | |
|
2 | onenon | |
|
3 | 1 2 | mp1i | |
4 | fvex | |
|
5 | simplr | |
|
6 | alephgeom | |
|
7 | 5 6 | sylib | |
8 | ssdomg | |
|
9 | 4 7 8 | mpsyl | |
10 | fvex | |
|
11 | ordom | |
|
12 | 2onn | |
|
13 | ordelss | |
|
14 | 11 12 13 | mp2an | |
15 | simpll | |
|
16 | alephgeom | |
|
17 | 15 16 | sylib | |
18 | 14 17 | sstrid | |
19 | ssdomg | |
|
20 | 10 18 19 | mpsyl | |
21 | alephord3 | |
|
22 | ssdomg | |
|
23 | 4 22 | ax-mp | |
24 | 21 23 | syl6bi | |
25 | 24 | imp | |
26 | 4 | canth2 | |
27 | sdomdom | |
|
28 | 26 27 | ax-mp | |
29 | domtr | |
|
30 | 25 28 29 | sylancl | |
31 | mappwen | |
|
32 | 3 9 20 30 31 | syl22anc | |
33 | 4 | pw2en | |
34 | enen2 | |
|
35 | 33 34 | ax-mp | |
36 | 32 35 | sylib | |