Metamath Proof Explorer


Theorem alephsuc3

Description: An alternate representation of a successor aleph. Compare alephsuc and alephsuc2 . Equality can be obtained by taking the card of the right-hand side then using alephcard and carden . (Contributed by NM, 23-Oct-2004)

Ref Expression
Assertion alephsuc3 AOnsucAxOn|xA

Proof

Step Hyp Ref Expression
1 alephsuc2 AOnsucA=xOn|xA
2 alephcard cardA=A
3 alephon AOn
4 onenon AOnAdomcard
5 3 4 ax-mp Adomcard
6 cardval2 AdomcardcardA=xOn|xA
7 5 6 ax-mp cardA=xOn|xA
8 2 7 eqtr3i A=xOn|xA
9 8 a1i AOnA=xOn|xA
10 1 9 difeq12d AOnsucAA=xOn|xAxOn|xA
11 difrab xOn|xAxOn|xA=xOn|xA¬xA
12 bren2 xAxA¬xA
13 12 rabbii xOn|xA=xOn|xA¬xA
14 11 13 eqtr4i xOn|xAxOn|xA=xOn|xA
15 10 14 eqtr2di AOnxOn|xA=sucAA
16 alephon sucAOn
17 onenon sucAOnsucAdomcard
18 16 17 mp1i AOnsucAdomcard
19 onsucb AOnsucAOn
20 alephgeom sucAOnωsucA
21 19 20 bitri AOnωsucA
22 fvex sucAV
23 ssdomg sucAVωsucAωsucA
24 22 23 ax-mp ωsucAωsucA
25 21 24 sylbi AOnωsucA
26 alephordilem1 AOnAsucA
27 infdif sucAdomcardωsucAAsucAsucAAsucA
28 18 25 26 27 syl3anc AOnsucAAsucA
29 15 28 eqbrtrd AOnxOn|xAsucA
30 29 ensymd AOnsucAxOn|xA