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	28 31	naddcld	$⊢ (((((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$
33		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$
34		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)$
35	32 33 34	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)$
36	19 24 35	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$
37	36	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$
38		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$
39		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$
40		ssralv	$⊢ A \subseteq B \to (\forall z \in B z + c \in x \to \forall z \in A z + c \in x)$
41	38 39 40	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$
42	37 41	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)$
43	42	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))$
44	43	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)\}$
45		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)\}$
46	44 45	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)\}$
47		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$
48		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)\}$
49	26 47 48	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)\}$
50		simplrr	$⊢ ((c \in On \land (A \in On \land B \in On)) \land A \subseteq B) \to B \in On$
51	50	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$
52		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)\}$
53	51 47 52	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)\}$
54	46 49 53	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$
55	54	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))$
56	55	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))$
57	56	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)))$
58	57	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)))$
59	14 58	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)))$
60	5 10 59	tfis3	$⊢ C \in On \to ((A \in On \land B \in On) \to (A \subseteq B \to A + C \subseteq B + C))$
61	60	com12	$⊢ (A \in On \land B \in On) \to (C \in On \to (A \subseteq B \to A + C \subseteq B + C))$
62	61	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