nnawordex

Description: Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002) (Revised by Mario Carneiro, 15-Nov-2014)

		Ref	Expression
	Assertion	nnawordex	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \leftrightarrow \exists x \in ω A +_{𝑜} x = B)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ y = B \to A +_{𝑜} y = A +_{𝑜} B$
2	1	sseq2d	$⊢ y = B \to (B \subseteq A +_{𝑜} y \leftrightarrow B \subseteq A +_{𝑜} B)$
3		simplr	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to B \in ω$
4		nnon	$⊢ B \in ω \to B \in On$
5	3 4	syl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to B \in On$
6		simpll	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to A \in ω$
7		nnaword2	$⊢ (B \in ω \land A \in ω) \to B \subseteq A +_{𝑜} B$
8	3 6 7	syl2anc	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to B \subseteq A +_{𝑜} B$
9	2 5 8	elrabd	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to B \in \{y \in On \| B \subseteq A +_{𝑜} y\}$
10		intss1	$⊢ B \in \{y \in On \| B \subseteq A +_{𝑜} y\} \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B$
11	9 10	syl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B$
12		ssrab2	$⊢ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq On$
13	9	ne0d	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to \{y \in On \| B \subseteq A +_{𝑜} y\} \neq \emptyset$
14		oninton	$⊢ (\{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq On \land \{y \in On \| B \subseteq A +_{𝑜} y\} \neq \emptyset) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in On$
15	12 13 14	sylancr	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in On$
16		eloni	$⊢ ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in On \to Ord ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
17	15 16	syl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to Ord ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
18		ordom	$⊢ Ord ω$
19		ordtr2	$⊢ (Ord ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \land Ord ω) \to ((⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B \land B \in ω) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in ω)$
20	17 18 19	sylancl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to ((⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B \land B \in ω) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in ω)$
21	11 3 20	mp2and	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in ω$
22		nna0	$⊢ A \in ω \to A +_{𝑜} \emptyset = A$
23	22	ad2antrr	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to A +_{𝑜} \emptyset = A$
24		simpr	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to A \subseteq B$
25	23 24	eqsstrd	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to A +_{𝑜} \emptyset \subseteq B$
26		oveq2	$⊢ ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = \emptyset \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = A +_{𝑜} \emptyset$
27	26	sseq1d	$⊢ ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = \emptyset \to (A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B \leftrightarrow A +_{𝑜} \emptyset \subseteq B)$
28	25 27	syl5ibrcom	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to (⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = \emptyset \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B)$
29		simprr	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x$
30	29	oveq2d	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = A +_{𝑜} suc x$
31	6	adantr	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A \in ω$
32		simprl	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to x \in ω$
33		nnasuc	$⊢ (A \in ω \land x \in ω) \to A +_{𝑜} suc x = suc (A +_{𝑜} x)$
34	31 32 33	syl2anc	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A +_{𝑜} suc x = suc (A +_{𝑜} x)$
35	30 34	eqtrd	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc (A +_{𝑜} x)$
36		nnord	$⊢ B \in ω \to Ord B$
37	3 36	syl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to Ord B$
38	37	adantr	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to Ord B$
39		nnon	$⊢ x \in ω \to x \in On$
40	39	adantr	$⊢ (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x) \to x \in On$
41		vex	$⊢ x \in V$
42	41	sucid	$⊢ x \in suc x$
43		simpr	$⊢ (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x$
44	42 43	eleqtrrid	$⊢ (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x) \to x \in ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
45		oveq2	$⊢ y = x \to A +_{𝑜} y = A +_{𝑜} x$
46	45	sseq2d	$⊢ y = x \to (B \subseteq A +_{𝑜} y \leftrightarrow B \subseteq A +_{𝑜} x)$
47	46	onnminsb	$⊢ x \in On \to (x \in ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \to \neg B \subseteq A +_{𝑜} x)$
48	40 44 47	sylc	$⊢ (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x) \to \neg B \subseteq A +_{𝑜} x$
49	48	adantl	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to \neg B \subseteq A +_{𝑜} x$
50		nnacl	$⊢ (A \in ω \land x \in ω) \to A +_{𝑜} x \in ω$
51	31 32 50	syl2anc	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A +_{𝑜} x \in ω$
52		nnord	$⊢ A +_{𝑜} x \in ω \to Ord (A +_{𝑜} x)$
53	51 52	syl	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to Ord (A +_{𝑜} x)$
54		ordtri1	$⊢ (Ord B \land Ord (A +_{𝑜} x)) \to (B \subseteq A +_{𝑜} x \leftrightarrow \neg A +_{𝑜} x \in B)$
55	38 53 54	syl2anc	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to (B \subseteq A +_{𝑜} x \leftrightarrow \neg A +_{𝑜} x \in B)$
56	55	con2bid	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to (A +_{𝑜} x \in B \leftrightarrow \neg B \subseteq A +_{𝑜} x)$
57	49 56	mpbird	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A +_{𝑜} x \in B$
58		ordsucss	$⊢ Ord B \to (A +_{𝑜} x \in B \to suc (A +_{𝑜} x) \subseteq B)$
59	38 57 58	sylc	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to suc (A +_{𝑜} x) \subseteq B$
60	35 59	eqsstrd	$⊢ (((A \in ω \land B \in ω) \land A \subseteq B) \land (x \in ω \land ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)) \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B$
61	60	rexlimdvaa	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to (\exists x \in ω ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B)$
62		nn0suc	$⊢ ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in ω \to (⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = \emptyset \lor \exists x \in ω ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)$
63	21 62	syl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to (⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = \emptyset \lor \exists x \in ω ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = suc x)$
64	28 61 63	mpjaod	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq B$
65		onint	$⊢ (\{y \in On \| B \subseteq A +_{𝑜} y\} \subseteq On \land \{y \in On \| B \subseteq A +_{𝑜} y\} \neq \emptyset) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in \{y \in On \| B \subseteq A +_{𝑜} y\}$
66	12 13 65	sylancr	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in \{y \in On \| B \subseteq A +_{𝑜} y\}$
67		nfrab1	$⊢ \underline{Ⅎ} y \{y \in On \| B \subseteq A +_{𝑜} y\}$
68	67	nfint	$⊢ \underline{Ⅎ} y ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
69		nfcv	$⊢ \underline{Ⅎ} y On$
70		nfcv	$⊢ \underline{Ⅎ} y B$
71		nfcv	$⊢ \underline{Ⅎ} y A$
72		nfcv	$⊢ \underline{Ⅎ} y +_{𝑜}$
73	71 72 68	nfov	$⊢ \underline{Ⅎ} y (A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\})$
74	70 73	nfss	$⊢ Ⅎ y B \subseteq A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
75		oveq2	$⊢ y = ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \to A +_{𝑜} y = A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
76	75	sseq2d	$⊢ y = ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \to (B \subseteq A +_{𝑜} y \leftrightarrow B \subseteq A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\})$
77	68 69 74 76	elrabf	$⊢ ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in \{y \in On \| B \subseteq A +_{𝑜} y\} \leftrightarrow (⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in On \land B \subseteq A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\})$
78	77	simprbi	$⊢ ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in \{y \in On \| B \subseteq A +_{𝑜} y\} \to B \subseteq A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
79	66 78	syl	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to B \subseteq A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
80	64 79	eqssd	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = B$
81		oveq2	$⊢ x = ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \to A +_{𝑜} x = A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\}$
82	81	eqeq1d	$⊢ x = ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \to (A +_{𝑜} x = B \leftrightarrow A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = B)$
83	82	rspcev	$⊢ (⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} \in ω \land A +_{𝑜} ⋂ \{y \in On \| B \subseteq A +_{𝑜} y\} = B) \to \exists x \in ω A +_{𝑜} x = B$
84	21 80 83	syl2anc	$⊢ ((A \in ω \land B \in ω) \land A \subseteq B) \to \exists x \in ω A +_{𝑜} x = B$
85	84	ex	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \to \exists x \in ω A +_{𝑜} x = B)$
86		nnaword1	$⊢ (A \in ω \land x \in ω) \to A \subseteq A +_{𝑜} x$
87	86	adantlr	$⊢ ((A \in ω \land B \in ω) \land x \in ω) \to A \subseteq A +_{𝑜} x$
88		sseq2	$⊢ A +_{𝑜} x = B \to (A \subseteq A +_{𝑜} x \leftrightarrow A \subseteq B)$
89	87 88	syl5ibcom	$⊢ ((A \in ω \land B \in ω) \land x \in ω) \to (A +_{𝑜} x = B \to A \subseteq B)$
90	89	rexlimdva	$⊢ (A \in ω \land B \in ω) \to (\exists x \in ω A +_{𝑜} x = B \to A \subseteq B)$
91	85 90	impbid	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \leftrightarrow \exists x \in ω A +_{𝑜} x = B)$

Metamath Proof Explorer

Theorem nnawordex

Proof