Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rankxplim Structured version   Unicode version

Theorem rankxplim 7803
 Description: The rank of a cross product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxpsuc 7806 for the successor case. (Contributed by NM, 19-Sep-2006.)
Hypotheses
Ref Expression
rankxplim.1
rankxplim.2
Assertion
Ref Expression
rankxplim

Proof of Theorem rankxplim
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwuni 4395 . . . . . . . . . 10
2 vex 2959 . . . . . . . . . . . 12
3 vex 2959 . . . . . . . . . . . 12
42, 3uniop 4459 . . . . . . . . . . 11
54pweqi 3803 . . . . . . . . . 10
61, 5sseqtri 3380 . . . . . . . . 9
7 pwuni 4395 . . . . . . . . . . 11
82, 3unipr 4029 . . . . . . . . . . . 12
98pweqi 3803 . . . . . . . . . . 11
107, 9sseqtri 3380 . . . . . . . . . 10
11 sspwb 4413 . . . . . . . . . 10
1210, 11mpbi 200 . . . . . . . . 9
136, 12sstri 3357 . . . . . . . 8
142, 3unex 4707 . . . . . . . . . . 11
1514pwex 4382 . . . . . . . . . 10
1615pwex 4382 . . . . . . . . 9
1716rankss 7775 . . . . . . . 8
1813, 17ax-mp 8 . . . . . . 7
19 rankxplim.1 . . . . . . . . . . 11
2019rankel 7765 . . . . . . . . . 10
21 rankxplim.2 . . . . . . . . . . 11
2221rankel 7765 . . . . . . . . . 10
232, 3, 19, 21rankelun 7798 . . . . . . . . . 10
2420, 22, 23syl2an 464 . . . . . . . . 9
2524adantl 453 . . . . . . . 8
26 ranklim 7770 . . . . . . . . . 10
27 ranklim 7770 . . . . . . . . . 10
2826, 27bitrd 245 . . . . . . . . 9
2928adantr 452 . . . . . . . 8
3025, 29mpbid 202 . . . . . . 7
31 rankon 7721 . . . . . . . 8
32 rankon 7721 . . . . . . . 8
33 ontr2 4628 . . . . . . . 8
3431, 32, 33mp2an 654 . . . . . . 7
3518, 30, 34sylancr 645 . . . . . 6
3631, 32onsucssi 4821 . . . . . 6
3735, 36sylib 189 . . . . 5
3837ralrimivva 2798 . . . 4
39 fveq2 5728 . . . . . . . 8
40 suceq 4646 . . . . . . . 8
4139, 40syl 16 . . . . . . 7
4241sseq1d 3375 . . . . . 6
4342ralxp 5016 . . . . 5
4419, 21xpex 4990 . . . . . 6
4544rankbnd 7794 . . . . 5
4643, 45bitr3i 243 . . . 4
4738, 46sylib 189 . . 3