Step |
Hyp |
Ref |
Expression |
1 |
|
rankxplim.1 |
|- A e. _V |
2 |
|
rankxplim.2 |
|- B e. _V |
3 |
|
limuni2 |
|- ( Lim ( rank ` ( A X. B ) ) -> Lim U. ( rank ` ( A X. B ) ) ) |
4 |
|
0ellim |
|- ( Lim U. ( rank ` ( A X. B ) ) -> (/) e. U. ( rank ` ( A X. B ) ) ) |
5 |
|
n0i |
|- ( (/) e. U. ( rank ` ( A X. B ) ) -> -. U. ( rank ` ( A X. B ) ) = (/) ) |
6 |
|
unieq |
|- ( ( rank ` ( A X. B ) ) = (/) -> U. ( rank ` ( A X. B ) ) = U. (/) ) |
7 |
|
uni0 |
|- U. (/) = (/) |
8 |
6 7
|
eqtrdi |
|- ( ( rank ` ( A X. B ) ) = (/) -> U. ( rank ` ( A X. B ) ) = (/) ) |
9 |
8
|
con3i |
|- ( -. U. ( rank ` ( A X. B ) ) = (/) -> -. ( rank ` ( A X. B ) ) = (/) ) |
10 |
4 5 9
|
3syl |
|- ( Lim U. ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) ) |
11 |
|
rankon |
|- ( rank ` ( A u. B ) ) e. On |
12 |
11
|
onsuci |
|- suc ( rank ` ( A u. B ) ) e. On |
13 |
12
|
onsuci |
|- suc suc ( rank ` ( A u. B ) ) e. On |
14 |
13
|
elexi |
|- suc suc ( rank ` ( A u. B ) ) e. _V |
15 |
14
|
sucid |
|- suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) |
16 |
13
|
onsuci |
|- suc suc suc ( rank ` ( A u. B ) ) e. On |
17 |
|
ontri1 |
|- ( ( suc suc suc ( rank ` ( A u. B ) ) e. On /\ suc suc ( rank ` ( A u. B ) ) e. On ) -> ( suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> -. suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) ) ) |
18 |
16 13 17
|
mp2an |
|- ( suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> -. suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) ) |
19 |
18
|
con2bii |
|- ( suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) <-> -. suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) ) |
20 |
15 19
|
mpbi |
|- -. suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) |
21 |
1 2
|
rankxpu |
|- ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) ) |
22 |
|
sstr |
|- ( ( suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) /\ ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) ) |
23 |
21 22
|
mpan2 |
|- ( suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) ) |
24 |
20 23
|
mto |
|- -. suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) |
25 |
|
reeanv |
|- ( E. x e. On E. y e. On ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) <-> ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) |
26 |
|
simprl |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( rank ` ( A u. B ) ) = suc x ) |
27 |
|
simpr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> ( rank ` ( A u. B ) ) = suc x ) |
28 |
|
df-ne |
|- ( ( A X. B ) =/= (/) <-> -. ( A X. B ) = (/) ) |
29 |
1 2
|
xpex |
|- ( A X. B ) e. _V |
30 |
29
|
rankeq0 |
|- ( ( A X. B ) = (/) <-> ( rank ` ( A X. B ) ) = (/) ) |
31 |
30
|
notbii |
|- ( -. ( A X. B ) = (/) <-> -. ( rank ` ( A X. B ) ) = (/) ) |
32 |
28 31
|
bitr2i |
|- ( -. ( rank ` ( A X. B ) ) = (/) <-> ( A X. B ) =/= (/) ) |
33 |
10 32
|
sylib |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( A X. B ) =/= (/) ) |
34 |
|
unixp |
|- ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) ) |
35 |
33 34
|
syl |
|- ( Lim U. ( rank ` ( A X. B ) ) -> U. U. ( A X. B ) = ( A u. B ) ) |
36 |
35
|
fveq2d |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) ) |
37 |
|
rankuni |
|- ( rank ` U. U. ( A X. B ) ) = U. ( rank ` U. ( A X. B ) ) |
38 |
|
rankuni |
|- ( rank ` U. ( A X. B ) ) = U. ( rank ` ( A X. B ) ) |
39 |
38
|
unieqi |
|- U. ( rank ` U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) |
40 |
37 39
|
eqtri |
|- ( rank ` U. U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) |
41 |
36 40
|
eqtr3di |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) ) |
42 |
|
eqimss |
|- ( ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) ) |
43 |
41 42
|
syl |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) ) |
44 |
43
|
adantr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) ) |
45 |
27 44
|
eqsstrrd |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> suc x C_ U. U. ( rank ` ( A X. B ) ) ) |
46 |
45
|
adantrr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x C_ U. U. ( rank ` ( A X. B ) ) ) |
47 |
|
limuni |
|- ( Lim U. ( rank ` ( A X. B ) ) -> U. ( rank ` ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) ) |
48 |
47
|
adantr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> U. ( rank ` ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) ) |
49 |
46 48
|
sseqtrrd |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x C_ U. ( rank ` ( A X. B ) ) ) |
50 |
|
vex |
|- x e. _V |
51 |
|
rankon |
|- ( rank ` ( A X. B ) ) e. On |
52 |
51
|
onordi |
|- Ord ( rank ` ( A X. B ) ) |
53 |
|
orduni |
|- ( Ord ( rank ` ( A X. B ) ) -> Ord U. ( rank ` ( A X. B ) ) ) |
54 |
52 53
|
ax-mp |
|- Ord U. ( rank ` ( A X. B ) ) |
55 |
|
ordelsuc |
|- ( ( x e. _V /\ Ord U. ( rank ` ( A X. B ) ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x C_ U. ( rank ` ( A X. B ) ) ) ) |
56 |
50 54 55
|
mp2an |
|- ( x e. U. ( rank ` ( A X. B ) ) <-> suc x C_ U. ( rank ` ( A X. B ) ) ) |
57 |
49 56
|
sylibr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> x e. U. ( rank ` ( A X. B ) ) ) |
58 |
|
limsuc |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x e. U. ( rank ` ( A X. B ) ) ) ) |
59 |
58
|
adantr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x e. U. ( rank ` ( A X. B ) ) ) ) |
60 |
57 59
|
mpbid |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x e. U. ( rank ` ( A X. B ) ) ) |
61 |
26 60
|
eqeltrd |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) |
62 |
|
limsuc |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) ) |
63 |
62
|
adantr |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) ) |
64 |
61 63
|
mpbid |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) |
65 |
|
ordsucelsuc |
|- ( Ord U. ( rank ` ( A X. B ) ) -> ( suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) ) ) |
66 |
54 65
|
ax-mp |
|- ( suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) ) |
67 |
64 66
|
sylib |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) ) |
68 |
|
onsucuni2 |
|- ( ( ( rank ` ( A X. B ) ) e. On /\ ( rank ` ( A X. B ) ) = suc y ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) ) |
69 |
51 68
|
mpan |
|- ( ( rank ` ( A X. B ) ) = suc y -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) ) |
70 |
69
|
ad2antll |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) ) |
71 |
67 70
|
eleqtrd |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc ( rank ` ( A u. B ) ) e. ( rank ` ( A X. B ) ) ) |
72 |
13 51
|
onsucssi |
|- ( suc suc ( rank ` ( A u. B ) ) e. ( rank ` ( A X. B ) ) <-> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) |
73 |
71 72
|
sylib |
|- ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) |
74 |
73
|
ex |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) ) |
75 |
74
|
a1d |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( ( x e. On /\ y e. On ) -> ( ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) ) ) |
76 |
75
|
rexlimdvv |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( E. x e. On E. y e. On ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) ) |
77 |
25 76
|
syl5bir |
|- ( Lim U. ( rank ` ( A X. B ) ) -> ( ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) ) |
78 |
24 77
|
mtoi |
|- ( Lim U. ( rank ` ( A X. B ) ) -> -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) |
79 |
|
ianor |
|- ( -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) <-> ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x \/ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) |
80 |
|
un00 |
|- ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) ) |
81 |
|
animorl |
|- ( ( A = (/) /\ B = (/) ) -> ( A = (/) \/ B = (/) ) ) |
82 |
80 81
|
sylbir |
|- ( ( A u. B ) = (/) -> ( A = (/) \/ B = (/) ) ) |
83 |
|
xpeq0 |
|- ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) ) |
84 |
82 83
|
sylibr |
|- ( ( A u. B ) = (/) -> ( A X. B ) = (/) ) |
85 |
84
|
con3i |
|- ( -. ( A X. B ) = (/) -> -. ( A u. B ) = (/) ) |
86 |
31 85
|
sylbir |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> -. ( A u. B ) = (/) ) |
87 |
1 2
|
unex |
|- ( A u. B ) e. _V |
88 |
87
|
rankeq0 |
|- ( ( A u. B ) = (/) <-> ( rank ` ( A u. B ) ) = (/) ) |
89 |
88
|
notbii |
|- ( -. ( A u. B ) = (/) <-> -. ( rank ` ( A u. B ) ) = (/) ) |
90 |
86 89
|
sylib |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> -. ( rank ` ( A u. B ) ) = (/) ) |
91 |
11
|
onordi |
|- Ord ( rank ` ( A u. B ) ) |
92 |
|
ordzsl |
|- ( Ord ( rank ` ( A u. B ) ) <-> ( ( rank ` ( A u. B ) ) = (/) \/ E. x e. On ( rank ` ( A u. B ) ) = suc x \/ Lim ( rank ` ( A u. B ) ) ) ) |
93 |
91 92
|
mpbi |
|- ( ( rank ` ( A u. B ) ) = (/) \/ E. x e. On ( rank ` ( A u. B ) ) = suc x \/ Lim ( rank ` ( A u. B ) ) ) |
94 |
93
|
3ori |
|- ( ( -. ( rank ` ( A u. B ) ) = (/) /\ -. E. x e. On ( rank ` ( A u. B ) ) = suc x ) -> Lim ( rank ` ( A u. B ) ) ) |
95 |
90 94
|
sylan |
|- ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. E. x e. On ( rank ` ( A u. B ) ) = suc x ) -> Lim ( rank ` ( A u. B ) ) ) |
96 |
95
|
ex |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x -> Lim ( rank ` ( A u. B ) ) ) ) |
97 |
|
ordzsl |
|- ( Ord ( rank ` ( A X. B ) ) <-> ( ( rank ` ( A X. B ) ) = (/) \/ E. y e. On ( rank ` ( A X. B ) ) = suc y \/ Lim ( rank ` ( A X. B ) ) ) ) |
98 |
52 97
|
mpbi |
|- ( ( rank ` ( A X. B ) ) = (/) \/ E. y e. On ( rank ` ( A X. B ) ) = suc y \/ Lim ( rank ` ( A X. B ) ) ) |
99 |
98
|
3ori |
|- ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> Lim ( rank ` ( A X. B ) ) ) |
100 |
99
|
ex |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. E. y e. On ( rank ` ( A X. B ) ) = suc y -> Lim ( rank ` ( A X. B ) ) ) ) |
101 |
96 100
|
orim12d |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x \/ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) ) |
102 |
79 101
|
syl5bi |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) ) |
103 |
102
|
imp |
|- ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) |
104 |
|
simpl |
|- ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> Lim ( rank ` ( A u. B ) ) ) |
105 |
30
|
necon3abii |
|- ( ( A X. B ) =/= (/) <-> -. ( rank ` ( A X. B ) ) = (/) ) |
106 |
1 2
|
rankxplim |
|- ( ( Lim ( rank ` ( A u. B ) ) /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) ) |
107 |
105 106
|
sylan2br |
|- ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) ) |
108 |
|
limeq |
|- ( ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) -> ( Lim ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) ) |
109 |
107 108
|
syl |
|- ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> ( Lim ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) ) |
110 |
104 109
|
mpbird |
|- ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> Lim ( rank ` ( A X. B ) ) ) |
111 |
110
|
expcom |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( Lim ( rank ` ( A u. B ) ) -> Lim ( rank ` ( A X. B ) ) ) ) |
112 |
|
idd |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A X. B ) ) ) ) |
113 |
111 112
|
jaod |
|- ( -. ( rank ` ( A X. B ) ) = (/) -> ( ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) -> Lim ( rank ` ( A X. B ) ) ) ) |
114 |
113
|
adantr |
|- ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> ( ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) -> Lim ( rank ` ( A X. B ) ) ) ) |
115 |
103 114
|
mpd |
|- ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> Lim ( rank ` ( A X. B ) ) ) |
116 |
10 78 115
|
syl2anc |
|- ( Lim U. ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A X. B ) ) ) |
117 |
3 116
|
impbii |
|- ( Lim ( rank ` ( A X. B ) ) <-> Lim U. ( rank ` ( A X. B ) ) ) |