ordsucun

Description: The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors. (Contributed by NM, 28-Nov-2003)

		Ref	Expression
	Assertion	ordsucun	$⊢ (Ord A \land Ord B) \to suc (A \cup B) = suc A \cup suc B$

Proof

Step	Hyp	Ref	Expression
1		ordun	$⊢ (Ord A \land Ord B) \to Ord (A \cup B)$
2		ordsuc	$⊢ Ord (A \cup B) \leftrightarrow Ord suc (A \cup B)$
3		ordelon	$⊢ (Ord suc (A \cup B) \land x \in suc (A \cup B)) \to x \in On$
4	3	ex	$⊢ Ord suc (A \cup B) \to (x \in suc (A \cup B) \to x \in On)$
5	2 4	sylbi	$⊢ Ord (A \cup B) \to (x \in suc (A \cup B) \to x \in On)$
6	1 5	syl	$⊢ (Ord A \land Ord B) \to (x \in suc (A \cup B) \to x \in On)$
7		ordsuc	$⊢ Ord A \leftrightarrow Ord suc A$
8		ordsuc	$⊢ Ord B \leftrightarrow Ord suc B$
9		ordun	$⊢ (Ord suc A \land Ord suc B) \to Ord (suc A \cup suc B)$
10		ordelon	$⊢ (Ord (suc A \cup suc B) \land x \in (suc A \cup suc B)) \to x \in On$
11	10	ex	$⊢ Ord (suc A \cup suc B) \to (x \in (suc A \cup suc B) \to x \in On)$
12	9 11	syl	$⊢ (Ord suc A \land Ord suc B) \to (x \in (suc A \cup suc B) \to x \in On)$
13	7 8 12	syl2anb	$⊢ (Ord A \land Ord B) \to (x \in (suc A \cup suc B) \to x \in On)$
14		ordssun	$⊢ (Ord A \land Ord B) \to (x \subseteq A \cup B \leftrightarrow (x \subseteq A \lor x \subseteq B))$
15	14	adantl	$⊢ (x \in On \land (Ord A \land Ord B)) \to (x \subseteq A \cup B \leftrightarrow (x \subseteq A \lor x \subseteq B))$
16		ordsssuc	$⊢ (x \in On \land Ord (A \cup B)) \to (x \subseteq A \cup B \leftrightarrow x \in suc (A \cup B))$
17	1 16	sylan2	$⊢ (x \in On \land (Ord A \land Ord B)) \to (x \subseteq A \cup B \leftrightarrow x \in suc (A \cup B))$
18		ordsssuc	$⊢ (x \in On \land Ord A) \to (x \subseteq A \leftrightarrow x \in suc A)$
19	18	adantrr	$⊢ (x \in On \land (Ord A \land Ord B)) \to (x \subseteq A \leftrightarrow x \in suc A)$
20		ordsssuc	$⊢ (x \in On \land Ord B) \to (x \subseteq B \leftrightarrow x \in suc B)$
21	20	adantrl	$⊢ (x \in On \land (Ord A \land Ord B)) \to (x \subseteq B \leftrightarrow x \in suc B)$
22	19 21	orbi12d	$⊢ (x \in On \land (Ord A \land Ord B)) \to ((x \subseteq A \lor x \subseteq B) \leftrightarrow (x \in suc A \lor x \in suc B))$
23	15 17 22	3bitr3d	$⊢ (x \in On \land (Ord A \land Ord B)) \to (x \in suc (A \cup B) \leftrightarrow (x \in suc A \lor x \in suc B))$
24		elun	$⊢ x \in (suc A \cup suc B) \leftrightarrow (x \in suc A \lor x \in suc B)$
25	23 24	bitr4di	$⊢ (x \in On \land (Ord A \land Ord B)) \to (x \in suc (A \cup B) \leftrightarrow x \in (suc A \cup suc B))$
26	25	expcom	$⊢ (Ord A \land Ord B) \to (x \in On \to (x \in suc (A \cup B) \leftrightarrow x \in (suc A \cup suc B)))$
27	6 13 26	pm5.21ndd	$⊢ (Ord A \land Ord B) \to (x \in suc (A \cup B) \leftrightarrow x \in (suc A \cup suc B))$
28	27	eqrdv	$⊢ (Ord A \land Ord B) \to suc (A \cup B) = suc A \cup suc B$

Metamath Proof Explorer

Theorem ordsucun

Proof