rankxplim3

Description: The rank of a Cartesian product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006)

	Ref	Expression
Hypotheses	rankxplim.1	$⊢ A \in V$
	rankxplim.2	$⊢ B \in V$
Assertion	rankxplim3	$⊢ Lim rank (A \times B) \leftrightarrow Lim ⋃ rank (A \times B)$

Proof

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

Metamath Proof Explorer

Theorem rankxplim3

Proof