Metamath Proof Explorer


Theorem alephexp1

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 AOnBOnABAB2𝑜B

Proof

Step Hyp Ref Expression
1 alephon BOn
2 onenon BOnBdomcard
3 1 2 mp1i AOnBOnABBdomcard
4 fvex BV
5 simplr AOnBOnABBOn
6 alephgeom BOnωB
7 5 6 sylib AOnBOnABωB
8 ssdomg BVωBωB
9 4 7 8 mpsyl AOnBOnABωB
10 fvex AV
11 ordom Ordω
12 2onn 2𝑜ω
13 ordelss Ordω2𝑜ω2𝑜ω
14 11 12 13 mp2an 2𝑜ω
15 simpll AOnBOnABAOn
16 alephgeom AOnωA
17 15 16 sylib AOnBOnABωA
18 14 17 sstrid AOnBOnAB2𝑜A
19 ssdomg AV2𝑜A2𝑜A
20 10 18 19 mpsyl AOnBOnAB2𝑜A
21 alephord3 AOnBOnABAB
22 ssdomg BVABAB
23 4 22 ax-mp ABAB
24 21 23 syl6bi AOnBOnABAB
25 24 imp AOnBOnABAB
26 4 canth2 B𝒫B
27 sdomdom B𝒫BB𝒫B
28 26 27 ax-mp B𝒫B
29 domtr ABB𝒫BA𝒫B
30 25 28 29 sylancl AOnBOnABA𝒫B
31 mappwen BdomcardωB2𝑜AA𝒫BAB𝒫B
32 3 9 20 30 31 syl22anc AOnBOnABAB𝒫B
33 4 pw2en 𝒫B2𝑜B
34 enen2 𝒫B2𝑜BAB𝒫BAB2𝑜B
35 33 34 ax-mp AB𝒫BAB2𝑜B
36 32 35 sylib AOnBOnABAB2𝑜B