naddssim

Description: Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024)

		Ref	Expression
	Assertion	naddssim	$⊢ (A \in On \land B \in On \land C \in On) \to (A \subseteq B \to A + C \subseteq B + C)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ c = d \to A + c = A + d$
2		oveq2	$⊢ c = d \to B + c = B + d$
3	1 2	sseq12d	$⊢ c = d \to (A + c \subseteq B + c \leftrightarrow A + d \subseteq B + d)$
4	3	imbi2d	$⊢ c = d \to ((A \subseteq B \to A + c \subseteq B + c) \leftrightarrow (A \subseteq B \to A + d \subseteq B + d))$
5	4	imbi2d	$⊢ c = d \to (((A \in On \land B \in On) \to (A \subseteq B \to A + c \subseteq B + c)) \leftrightarrow ((A \in On \land B \in On) \to (A \subseteq B \to A + d \subseteq B + d)))$
6		oveq2	$⊢ c = C \to A + c = A + C$
7		oveq2	$⊢ c = C \to B + c = B + C$
8	6 7	sseq12d	$⊢ c = C \to (A + c \subseteq B + c \leftrightarrow A + C \subseteq B + C)$
9	8	imbi2d	$⊢ c = C \to ((A \subseteq B \to A + c \subseteq B + c) \leftrightarrow (A \subseteq B \to A + C \subseteq B + C))$
10	9	imbi2d	$⊢ c = C \to (((A \in On \land B \in On) \to (A \subseteq B \to A + c \subseteq B + c)) \leftrightarrow ((A \in On \land B \in On) \to (A \subseteq B \to A + C \subseteq B + C)))$
11		r19.21v	$⊢ \forall d \in c ((A \in On \land B \in On) \to (A \subseteq B \to A + d \subseteq B + d)) \leftrightarrow ((A \in On \land B \in On) \to \forall d \in c (A \subseteq B \to A + d \subseteq B + d))$
12		r19.21v	$⊢ \forall d \in c (A \subseteq B \to A + d \subseteq B + d) \leftrightarrow (A \subseteq B \to \forall d \in c A + d \subseteq B + d)$
13	12	imbi2i	$⊢ ((A \in On \land B \in On) \to \forall d \in c (A \subseteq B \to A + d \subseteq B + d)) \leftrightarrow ((A \in On \land B \in On) \to (A \subseteq B \to \forall d \in c A + d \subseteq B + d))$
14	11 13	bitri	$⊢ \forall d \in c ((A \in On \land B \in On) \to (A \subseteq B \to A + d \subseteq B + d)) \leftrightarrow ((A \in On \land B \in On) \to (A \subseteq B \to \forall d \in c A + d \subseteq B + d))$
15		oveq2	$⊢ d = w \to A + d = A + w$
16		oveq2	$⊢ d = w \to B + d = B + w$
17	15 16	sseq12d	$⊢ d = w \to (A + d \subseteq B + d \leftrightarrow A + w \subseteq B + w)$
18	17	rspccva	$⊢ (\forall d \in c A + d \subseteq B + d \land w \in c) \to A + w \subseteq B + w$
19	18	ad4ant24	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to A + w \subseteq B + w$
20		simprrl	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to \forall y \in c B + y \in x$
21		oveq2	$⊢ y = w \to B + y = B + w$
22	21	eleq1d	$⊢ y = w \to (B + y \in x \leftrightarrow B + w \in x)$
23	22	rspccva	$⊢ (\forall y \in c B + y \in x \land w \in c) \to B + w \in x$
24	20 23	sylan	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to B + w \in x$
25		simplrl	$⊢ ((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \to A \in On$
26	25	adantr	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to A \in On$
27	26	adantr	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to A \in On$
28	27	adantr	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to A \in On$
29		simp-4l	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to c \in On$
30		onelon	$⊢ (c \in On \land w \in c) \to w \in On$
31	29 30	sylan	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to w \in On$
32		naddcl	$⊢ (A \in On \land w \in On) \to A + w \in On$
33	28 31 32	syl2anc	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to A + w \in On$
34		simplrl	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to x \in On$
35		ontr2	$⊢ (A + w \in On \land x \in On) \to ((A + w \subseteq B + w \land B + w \in x) \to A + w \in x)$
36	33 34 35	syl2anc	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to ((A + w \subseteq B + w \land B + w \in x) \to A + w \in x)$
37	19 24 36	mp2and	$⊢ (((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \land w \in c) \to A + w \in x$
38	37	ralrimiva	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to \forall w \in c A + w \in x$
39		simpllr	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to A \subseteq B$
40		simprrr	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to \forall z \in B z + c \in x$
41		ssralv	$⊢ A \subseteq B \to (\forall z \in B z + c \in x \to \forall z \in A z + c \in x)$
42	39 40 41	sylc	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to \forall z \in A z + c \in x$
43	38 42	jca	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land (x \in On \land (\forall y \in c B + y \in x \land \forall z \in B z + c \in x))) \to (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)$
44	43	expr	$⊢ ((((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \land x \in On) \to ((\forall y \in c B + y \in x \land \forall z \in B z + c \in x) \to (\forall w \in c A + w \in x \land \forall z \in A z + c \in x))$
45	44	ss2rabdv	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to \{x \in On \| (\forall y \in c B + y \in x \land \forall z \in B z + c \in x)\} \subseteq \{x \in On \| (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)\}$
46		intss	$⊢ \{x \in On \| (\forall y \in c B + y \in x \land \forall z \in B z + c \in x)\} \subseteq \{x \in On \| (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)\} \to ⋂ \{x \in On \| (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)\} \subseteq ⋂ \{x \in On \| (\forall y \in c B + y \in x \land \forall z \in B z + c \in x)\}$
47	45 46	syl	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to ⋂ \{x \in On \| (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)\} \subseteq ⋂ \{x \in On \| (\forall y \in c B + y \in x \land \forall z \in B z + c \in x)\}$
48		simplll	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to c \in On$
49		naddov2	$⊢ (A \in On \land c \in On) \to A + c = ⋂ \{x \in On \| (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)\}$
50	26 48 49	syl2anc	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to A + c = ⋂ \{x \in On \| (\forall w \in c A + w \in x \land \forall z \in A z + c \in x)\}$
51		simplrr	$⊢ ((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \to B \in On$
52	51	adantr	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to B \in On$
53		naddov2	$⊢ (B \in On \land c \in On) \to B + c = ⋂ \{x \in On \| (\forall y \in c B + y \in x \land \forall z \in B z + c \in x)\}$
54	52 48 53	syl2anc	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to B + c = ⋂ \{x \in On \| (\forall y \in c B + y \in x \land \forall z \in B z + c \in x)\}$
55	47 50 54	3sstr4d	$⊢ (((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \land \forall d \in c A + d \subseteq B + d) \to A + c \subseteq B + c$
56	55	exp31	$⊢ (c \in On \land (A \in On \land B \in On)) \to (A \subseteq B \to (\forall d \in c A + d \subseteq B + d \to A + c \subseteq B + c))$
57	56	a2d	$⊢ (c \in On \land (A \in On \land B \in On)) \to ((A \subseteq B \to \forall d \in c A + d \subseteq B + d) \to (A \subseteq B \to A + c \subseteq B + c))$
58	57	ex	$⊢ c \in On \to ((A \in On \land B \in On) \to ((A \subseteq B \to \forall d \in c A + d \subseteq B + d) \to (A \subseteq B \to A + c \subseteq B + c)))$
59	58	a2d	$⊢ c \in On \to (((A \in On \land B \in On) \to (A \subseteq B \to \forall d \in c A + d \subseteq B + d)) \to ((A \in On \land B \in On) \to (A \subseteq B \to A + c \subseteq B + c)))$
60	14 59	biimtrid	$⊢ c \in On \to (\forall d \in c ((A \in On \land B \in On) \to (A \subseteq B \to A + d \subseteq B + d)) \to ((A \in On \land B \in On) \to (A \subseteq B \to A + c \subseteq B + c)))$
61	5 10 60	tfis3	$⊢ C \in On \to ((A \in On \land B \in On) \to (A \subseteq B \to A + C \subseteq B + C))$
62	61	com12	$⊢ (A \in On \land B \in On) \to (C \in On \to (A \subseteq B \to A + C \subseteq B + C))$
63	62	3impia	$⊢ (A \in On \land B \in On \land C \in On) \to (A \subseteq B \to A + C \subseteq B + C)$

Metamath Proof Explorer

Theorem naddssim

Proof