Theorem rankxplim3 4724

Description: The rank of a cross product is a limit ordinal iff its union is.

Hypotheses

Ref	Expression
rankxplim.1	|- A e. V
rankxplim.2	|- B e. V

Assertion

Ref	Expression
rankxplim3	|- (Lim (rank` (A X. B)) <-> Lim U.(rank` (A X. B)))

Proof of Theorem rankxplim3

Step	Hyp	Ref	Expression
1		limuni2 3036	. 2 |- (Lim (rank` (A X. B)) -> Lim U.(rank` (A X. B)))
2		rankon 4681	. . . . . . . . . . . 12 |- (rank` (A u. B)) e. On
3	2	onord 3101	. . . . . . . . . . 11 |- Ord (rank` (A u. B))
4		ordzsl 3122	. . . . . . . . . . 11 |- (Ord (rank` (A u. B)) <-> ((rank` (A u. B)) = (/) \/ E.x e. On (rank` (A u. B)) = suc x \/ Lim (rank` (A u. B))))
5	3, 4	mpbi 189	. . . . . . . . . 10 |- ((rank` (A u. B)) = (/) \/ E.x e. On (rank` (A u. B)) = suc x \/ Lim (rank` (A u. B)))
6	5	3ori 887	. . . . . . . . 9 |- ((-. (rank` (A u. B)) = (/) /\ -. E.x e. On (rank` (A u. B)) = suc x) -> Lim (rank` (A u. B)))
7		un00 2310	. . . . . . . . . . . . 13 |- ((A = (/) /\ B = (/)) <-> (A u. B) = (/))
8		olc 268	. . . . . . . . . . . . . 14 |- (B = (/) -> (A = (/) \/ B = (/)))
9	8	adantl 390	. . . . . . . . . . . . 13 |- ((A = (/) /\ B = (/)) -> (A = (/) \/ B = (/)))
10	7, 9	sylbir 201	. . . . . . . . . . . 12 |- ((A u. B) = (/) -> (A = (/) \/ B = (/)))
11		xpeq0 3473	. . . . . . . . . . . 12 |- ((A X. B) = (/) <-> (A = (/) \/ B = (/)))
12	10, 11	sylibr 200	. . . . . . . . . . 11 |- ((A u. B) = (/) -> (A X. B) = (/))
13	12	con3i 98	. . . . . . . . . 10 |- (-. (A X. B) = (/) -> -. (A u. B) = (/))
14		rankxplim.1	. . . . . . . . . . . . 13 |- A e. V
15		rankxplim.2	. . . . . . . . . . . . 13 |- B e. V
16	14, 15	xpex 3266	. . . . . . . . . . . 12 |- (A X. B) e. V
17	16	rankeq0 4706	. . . . . . . . . . 11 |- ((A X. B) = (/) <-> (rank` (A X. B)) = (/))
18	17	negbii 187	. . . . . . . . . 10 |- (-. (A X. B) = (/) <-> -. (rank` (A X. B)) = (/))
19	14, 15	unex 2878	. . . . . . . . . . . 12 |- (A u. B) e. V
20	19	rankeq0 4706	. . . . . . . . . . 11 |- ((A u. B) = (/) <-> (rank` (A u. B)) = (/))
21	20	negbii 187	. . . . . . . . . 10 |- (-. (A u. B) = (/) <-> -. (rank` (A u. B)) = (/))
22	13, 18, 21	3imtr3 218	. . . . . . . . 9 |- (-. (rank` (A X. B)) = (/) -> -. (rank` (A u. B)) = (/))
23	6, 22	sylan 450	. . . . . . . 8 |- ((-. (rank` (A X. B)) = (/) /\ -. E.x e. On (rank` (A u. B)) = suc x) -> Lim (rank` (A u. B)))
24	23	ex 373	. . . . . . 7 |- (-. (rank` (A X. B)) = (/) -> (-. E.x e. On (rank` (A u. B)) = suc x -> Lim (rank` (A u. B))))
25		rankon 4681	. . . . . . . . . . 11 |- (rank` (A X. B)) e. On
26	25	onord 3101	. . . . . . . . . 10 |- Ord (rank` (A X. B))
27		ordzsl 3122	. . . . . . . . . 10 |- (Ord (rank` (A X. B)) <-> ((rank` (A X. B)) = (/) \/ E.y e. On (rank` (A X. B)) = suc y \/ Lim (rank` (A X. B))))
28	26, 27	mpbi 189	. . . . . . . . 9 |- ((rank` (A X. B)) = (/) \/ E.y e. On (rank` (A X. B)) = suc y \/ Lim (rank` (A X. B)))
29	28	3ori 887	. . . . . . . 8 |- ((-. (rank` (A X. B)) = (/) /\ -. E.y e. On (rank` (A X. B)) = suc y) -> Lim (rank` (A X. B)))
30	29	ex 373	. . . . . . 7 |- (-. (rank` (A X. B)) = (/) -> (-. E.y e. On (rank` (A X. B)) = suc y -> Lim (rank` (A X. B))))
31	24, 30	orim12d 567	. . . . . 6 |- (-. (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)))))
32		ianor 305	. . . . . 6 |- (-. (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))
33	31, 32	syl5ib 206	. . . . 5 |- (-. (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)))))
34	33	imp 350	. . . 4 |- ((-. (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))))
35		pm3.26 319	. . . . . . . 8 |- ((Lim (rank` (A u. B)) /\ -. (rank` (A X. B)) = (/)) -> Lim (rank` (A u. B)))
36	14, 15	rankxplim 4722	. . . . . . . . . 10 |- ((Lim (rank` (A u. B)) /\ (A X. B) =/= (/)) -> (rank` (A X. B)) = (rank` (A u. B)))
37	17	necon3abii 1599	. . . . . . . . . 10 |- ((A X. B) =/= (/) <-> -. (rank` (A X. B)) = (/))
38	36, 37	sylan2br 455	. . . . . . . . 9 |- ((Lim (rank` (A u. B)) /\ -. (rank` (A X. B)) = (/)) -> (rank` (A X. B)) = (rank` (A u. B)))
39		limeq 2966	. . . . . . . . 9 |- ((rank` (A X. B)) = (rank` (A u. B)) -> (Lim (rank` (A X. B)) <-> Lim (rank` (A u. B))))
40	38, 39	syl 10	. . . . . . . 8 |- ((Lim (rank` (A u. B)) /\ -. (rank` (A X. B)) = (/)) -> (Lim (rank` (A X. B)) <-> Lim (rank` (A u. B))))
41	35, 40	mpbird 196	. . . . . . 7 |- ((Lim (rank` (A u. B)) /\ -. (rank` (A X. B)) = (/)) -> Lim (rank` (A X. B)))
42	41	expcom 374	. . . . . 6 |- (-. (rank` (A X. B)) = (/) -> (Lim (rank` (A u. B)) -> Lim (rank` (A X. B))))
43		idd 61	. . . . . 6 |- (-. (rank` (A X. B)) = (/) -> (Lim (rank` (A X. B)) -> Lim (rank` (A X. B))))
44	42, 43	jaod 426	. . . . 5 |- (-. (rank` (A X. B)) = (/) -> ((Lim (rank` (A u. B)) \/ Lim (rank` (A X. B))) -> Lim (rank` (A X. B))))
45	44	adantr 391	. . . 4 |- ((-. (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))))
46	34, 45	mpd 26	. . 3 |- ((-. (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)))
47		0ellim 3037	. . . 4 |- (Lim U.(rank` (A X. B)) -> (/) e. U.(rank` (A X. B)))
48		n0i 2288	. . . 4 |- ((/) e. U.(rank` (A X. B)) -> -. U.(rank` (A X. B)) = (/))
49		unieq 2514	. . . . . 6 |- ((rank` (A X. B)) = (/) -> U.(rank` (A X. B)) = U.(/))
50		uni0 2529	. . . . . 6 |- U.(/) = (/)
51	49, 50	syl6eq 1526	. . . . 5 |- ((rank` (A X. B)) = (/) -> U.(rank` (A X. B)) = (/))
52	51	con3i 98	. . . 4 |- (-. U.(rank` (A X. B)) = (/) -> -. (rank` (A X. B)) = (/))
53	47, 48, 52	3syl 20	. . 3 |- (Lim U.(rank` (A X. B)) -> -. (rank` (A X. B)) = (/))
54	2	onsuc 3111	. . . . . . . . 9 |- suc (rank` (A u. B)) e. On
55	54	onsuc 3111	. . . . . . . 8 |- suc suc (rank` (A u. B)) e. On
56	55	elisseti 1821	. . . . . . 7 |- suc suc (rank` (A u. B)) e. V
57	56	sucid 3057	. . . . . 6 |- suc suc (rank` (A u. B)) e. suc suc suc (rank` (A u. B))
58	55	onsuc 3111	. . . . . . . 8 |- suc suc suc (rank` (A u. B)) e. On
59		ontri1 2987	. . . . . . . 8 |- ((suc suc suc (rank` (A u. B)) e. On /\ suc suc (rank` (A u. B)) e. On) -> (suc suc suc <