nadd2rabtr

Description: The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024)

		Ref	Expression
	Assertion	nadd2rabtr	$⊢ (Ord A \land B \in On \land C \in On) \to Tr \{x \in A \| B + x \in C\}$

Proof

Step	Hyp	Ref	Expression
1		simpll1	$⊢ (((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \to Ord A$
2		simplr	$⊢ (((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \to y \in A$
3		ordelss	$⊢ (Ord A \land y \in A) \to y \subseteq A$
4	1 2 3	syl2anc	$⊢ (((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \to y \subseteq A$
5		simpll3	$⊢ (((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \to C \in On$
6	5	adantr	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to C \in On$
7		simpr	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to x \in y$
8	1	adantr	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to Ord A$
9		simpllr	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to y \in A$
10		ordelon	$⊢ (Ord A \land y \in A) \to y \in On$
11	8 9 10	syl2anc	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to y \in On$
12		onelon	$⊢ (y \in On \land x \in y) \to x \in On$
13	11 7 12	syl2anc	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to x \in On$
14		simpll2	$⊢ (((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \to B \in On$
15	14	adantr	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to B \in On$
16		naddel2	$⊢ (x \in On \land y \in On \land B \in On) \to (x \in y \leftrightarrow B + x \in (B + y))$
17	13 11 15 16	syl3anc	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to (x \in y \leftrightarrow B + x \in (B + y))$
18	7 17	mpbid	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to B + x \in (B + y)$
19		simplr	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to B + y \in C$
20	18 19	jca	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to (B + x \in (B + y) \land B + y \in C)$
21		ontr1	$⊢ C \in On \to ((B + x \in (B + y) \land B + y \in C) \to B + x \in C)$
22	6 20 21	sylc	$⊢ ((((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \land x \in y) \to B + x \in C$
23	4 22	ssrabdv	$⊢ (((Ord A \land B \in On \land C \in On) \land y \in A) \land B + y \in C) \to y \subseteq \{x \in A \| B + x \in C\}$
24	23	ex	$⊢ ((Ord A \land B \in On \land C \in On) \land y \in A) \to (B + y \in C \to y \subseteq \{x \in A \| B + x \in C\})$
25	24	ralrimiva	$⊢ (Ord A \land B \in On \land C \in On) \to \forall y \in A (B + y \in C \to y \subseteq \{x \in A \| B + x \in C\})$
26		oveq2	$⊢ x = y \to B + x = B + y$
27	26	eleq1d	$⊢ x = y \to (B + x \in C \leftrightarrow B + y \in C)$
28	27	ralrab	$⊢ \forall y \in \{x \in A \| B + x \in C\} y \subseteq \{x \in A \| B + x \in C\} \leftrightarrow \forall y \in A (B + y \in C \to y \subseteq \{x \in A \| B + x \in C\})$
29	25 28	sylibr	$⊢ (Ord A \land B \in On \land C \in On) \to \forall y \in \{x \in A \| B + x \in C\} y \subseteq \{x \in A \| B + x \in C\}$
30		dftr3	$⊢ Tr \{x \in A \| B + x \in C\} \leftrightarrow \forall y \in \{x \in A \| B + x \in C\} y \subseteq \{x \in A \| B + x \in C\}$
31	29 30	sylibr	$⊢ (Ord A \land B \in On \land C \in On) \to Tr \{x \in A \| B + x \in C\}$

Metamath Proof Explorer

Theorem nadd2rabtr

Proof