onsucunipr

Description: The successor to the union of any pair of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025)

		Ref	Expression
	Assertion	onsucunipr	$⊢ (A \in On \land B \in On) \to suc ⋃ \{A, B\} = ⋃ \{suc A, suc B\}$

Proof

Step	Hyp	Ref	Expression
1		ssequn1	$⊢ A \subseteq B \leftrightarrow A \cup B = B$
2		suceq	$⊢ A \cup B = B \to suc (A \cup B) = suc B$
3	1 2	sylbi	$⊢ A \subseteq B \to suc (A \cup B) = suc B$
4	3	adantl	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to suc (A \cup B) = suc B$
5		onsucwordi	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to suc A \subseteq suc B)$
6	5	imp	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to suc A \subseteq suc B$
7		ssequn1	$⊢ suc A \subseteq suc B \leftrightarrow suc A \cup suc B = suc B$
8	6 7	sylib	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to suc A \cup suc B = suc B$
9	4 8	eqtr4d	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to suc (A \cup B) = suc A \cup suc B$
10		ssequn2	$⊢ B \subseteq A \leftrightarrow A \cup B = A$
11		suceq	$⊢ A \cup B = A \to suc (A \cup B) = suc A$
12	10 11	sylbi	$⊢ B \subseteq A \to suc (A \cup B) = suc A$
13	12	adantl	$⊢ ((A \in On \land B \in On) \land B \subseteq A) \to suc (A \cup B) = suc A$
14		onsucwordi	$⊢ (B \in On \land A \in On) \to (B \subseteq A \to suc B \subseteq suc A)$
15	14	ancoms	$⊢ (A \in On \land B \in On) \to (B \subseteq A \to suc B \subseteq suc A)$
16	15	imp	$⊢ ((A \in On \land B \in On) \land B \subseteq A) \to suc B \subseteq suc A$
17		ssequn2	$⊢ suc B \subseteq suc A \leftrightarrow suc A \cup suc B = suc A$
18	16 17	sylib	$⊢ ((A \in On \land B \in On) \land B \subseteq A) \to suc A \cup suc B = suc A$
19	13 18	eqtr4d	$⊢ ((A \in On \land B \in On) \land B \subseteq A) \to suc (A \cup B) = suc A \cup suc B$
20		eloni	$⊢ A \in On \to Ord A$
21		eloni	$⊢ B \in On \to Ord B$
22		ordtri2or2	$⊢ (Ord A \land Ord B) \to (A \subseteq B \lor B \subseteq A)$
23	20 21 22	syl2an	$⊢ (A \in On \land B \in On) \to (A \subseteq B \lor B \subseteq A)$
24	9 19 23	mpjaodan	$⊢ (A \in On \land B \in On) \to suc (A \cup B) = suc A \cup suc B$
25		uniprg	$⊢ (A \in On \land B \in On) \to ⋃ \{A, B\} = A \cup B$
26		suceq	$⊢ ⋃ \{A, B\} = A \cup B \to suc ⋃ \{A, B\} = suc (A \cup B)$
27	25 26	syl	$⊢ (A \in On \land B \in On) \to suc ⋃ \{A, B\} = suc (A \cup B)$
28		onsuc	$⊢ A \in On \to suc A \in On$
29		onsuc	$⊢ B \in On \to suc B \in On$
30		uniprg	$⊢ (suc A \in On \land suc B \in On) \to ⋃ \{suc A, suc B\} = suc A \cup suc B$
31	28 29 30	syl2an	$⊢ (A \in On \land B \in On) \to ⋃ \{suc A, suc B\} = suc A \cup suc B$
32	24 27 31	3eqtr4d	$⊢ (A \in On \land B \in On) \to suc ⋃ \{A, B\} = ⋃ \{suc A, suc B\}$

Metamath Proof Explorer

Theorem onsucunipr

Proof