oewordri

Description: Weak ordering property of ordinal exponentiation. Proposition 8.35 of TakeutiZaring p. 68. (Contributed by NM, 6-Jan-2005)

		Ref	Expression
	Assertion	oewordri	$⊢ (B \in On \land C \in On) \to (A \in B \to A ↑_{𝑜} C \subseteq B ↑_{𝑜} C)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to A ↑_{𝑜} x = A ↑_{𝑜} \emptyset$
2		oveq2	$⊢ x = \emptyset \to B ↑_{𝑜} x = B ↑_{𝑜} \emptyset$
3	1 2	sseq12d	$⊢ x = \emptyset \to (A ↑_{𝑜} x \subseteq B ↑_{𝑜} x \leftrightarrow A ↑_{𝑜} \emptyset \subseteq B ↑_{𝑜} \emptyset)$
4		oveq2	$⊢ x = y \to A ↑_{𝑜} x = A ↑_{𝑜} y$
5		oveq2	$⊢ x = y \to B ↑_{𝑜} x = B ↑_{𝑜} y$
6	4 5	sseq12d	$⊢ x = y \to (A ↑_{𝑜} x \subseteq B ↑_{𝑜} x \leftrightarrow A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)$
7		oveq2	$⊢ x = suc y \to A ↑_{𝑜} x = A ↑_{𝑜} suc y$
8		oveq2	$⊢ x = suc y \to B ↑_{𝑜} x = B ↑_{𝑜} suc y$
9	7 8	sseq12d	$⊢ x = suc y \to (A ↑_{𝑜} x \subseteq B ↑_{𝑜} x \leftrightarrow A ↑_{𝑜} suc y \subseteq B ↑_{𝑜} suc y)$
10		oveq2	$⊢ x = C \to A ↑_{𝑜} x = A ↑_{𝑜} C$
11		oveq2	$⊢ x = C \to B ↑_{𝑜} x = B ↑_{𝑜} C$
12	10 11	sseq12d	$⊢ x = C \to (A ↑_{𝑜} x \subseteq B ↑_{𝑜} x \leftrightarrow A ↑_{𝑜} C \subseteq B ↑_{𝑜} C)$
13		onelon	$⊢ (B \in On \land A \in B) \to A \in On$
14		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
15	13 14	syl	$⊢ (B \in On \land A \in B) \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
16		oe0	$⊢ B \in On \to B ↑_{𝑜} \emptyset = 1_{𝑜}$
17	16	adantr	$⊢ (B \in On \land A \in B) \to B ↑_{𝑜} \emptyset = 1_{𝑜}$
18	15 17	eqtr4d	$⊢ (B \in On \land A \in B) \to A ↑_{𝑜} \emptyset = B ↑_{𝑜} \emptyset$
19		eqimss	$⊢ A ↑_{𝑜} \emptyset = B ↑_{𝑜} \emptyset \to A ↑_{𝑜} \emptyset \subseteq B ↑_{𝑜} \emptyset$
20	18 19	syl	$⊢ (B \in On \land A \in B) \to A ↑_{𝑜} \emptyset \subseteq B ↑_{𝑜} \emptyset$
21		simpl	$⊢ (B \in On \land A \in B) \to B \in On$
22		onelss	$⊢ B \in On \to (A \in B \to A \subseteq B)$
23	22	imp	$⊢ (B \in On \land A \in B) \to A \subseteq B$
24	13 21 23	jca31	$⊢ (B \in On \land A \in B) \to ((A \in On \land B \in On) \land A \subseteq B)$
25		oecl	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} y \in On$
26	25	3adant2	$⊢ (A \in On \land B \in On \land y \in On) \to A ↑_{𝑜} y \in On$
27		oecl	$⊢ (B \in On \land y \in On) \to B ↑_{𝑜} y \in On$
28	27	3adant1	$⊢ (A \in On \land B \in On \land y \in On) \to B ↑_{𝑜} y \in On$
29		simp1	$⊢ (A \in On \land B \in On \land y \in On) \to A \in On$
30		omwordri	$⊢ (A ↑_{𝑜} y \in On \land B ↑_{𝑜} y \in On \land A \in On) \to (A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to (A ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} A)$
31	26 28 29 30	syl3anc	$⊢ (A \in On \land B \in On \land y \in On) \to (A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to (A ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} A)$
32	31	imp	$⊢ ((A \in On \land B \in On \land y \in On) \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y) \to (A ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} A$
33	32	adantrl	$⊢ ((A \in On \land B \in On \land y \in On) \land (A \subseteq B \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)) \to (A ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} A$
34		omwordi	$⊢ (A \in On \land B \in On \land B ↑_{𝑜} y \in On) \to (A \subseteq B \to (B ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} B)$
35	28 34	syld3an3	$⊢ (A \in On \land B \in On \land y \in On) \to (A \subseteq B \to (B ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} B)$
36	35	imp	$⊢ ((A \in On \land B \in On \land y \in On) \land A \subseteq B) \to (B ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} B$
37	36	adantrr	$⊢ ((A \in On \land B \in On \land y \in On) \land (A \subseteq B \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)) \to (B ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} B$
38	33 37	sstrd	$⊢ ((A \in On \land B \in On \land y \in On) \land (A \subseteq B \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)) \to (A ↑_{𝑜} y) \cdot_{𝑜} A \subseteq (B ↑_{𝑜} y) \cdot_{𝑜} B$
39		oesuc	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
40	39	3adant2	$⊢ (A \in On \land B \in On \land y \in On) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
41	40	adantr	$⊢ ((A \in On \land B \in On \land y \in On) \land (A \subseteq B \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
42		oesuc	$⊢ (B \in On \land y \in On) \to B ↑_{𝑜} suc y = (B ↑_{𝑜} y) \cdot_{𝑜} B$
43	42	3adant1	$⊢ (A \in On \land B \in On \land y \in On) \to B ↑_{𝑜} suc y = (B ↑_{𝑜} y) \cdot_{𝑜} B$
44	43	adantr	$⊢ ((A \in On \land B \in On \land y \in On) \land (A \subseteq B \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)) \to B ↑_{𝑜} suc y = (B ↑_{𝑜} y) \cdot_{𝑜} B$
45	38 41 44	3sstr4d	$⊢ ((A \in On \land B \in On \land y \in On) \land (A \subseteq B \land A ↑_{𝑜} y \subseteq B ↑_{𝑜} y)) \to A ↑_{𝑜} suc y \subseteq B ↑_{𝑜} suc y$
46	45	exp520	$⊢ A \in On \to (B \in On \to (y \in On \to (A \subseteq B \to (A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} suc y \subseteq B ↑_{𝑜} suc y))))$
47	46	com3r	$⊢ y \in On \to (A \in On \to (B \in On \to (A \subseteq B \to (A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} suc y \subseteq B ↑_{𝑜} suc y))))$
48	47	imp4c	$⊢ y \in On \to (((A \in On \land B \in On) \land A \subseteq B) \to (A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} suc y \subseteq B ↑_{𝑜} suc y))$
49	24 48	syl5	$⊢ y \in On \to ((B \in On \land A \in B) \to (A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} suc y \subseteq B ↑_{𝑜} suc y))$
50		vex	$⊢ x \in V$
51		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
52	50 51	mpan	$⊢ Lim x \to x \in On$
53		0ellim	$⊢ Lim x \to \emptyset \in x$
54		oe0m1	$⊢ x \in On \to (\emptyset \in x \leftrightarrow \emptyset ↑_{𝑜} x = \emptyset)$
55	54	biimpa	$⊢ (x \in On \land \emptyset \in x) \to \emptyset ↑_{𝑜} x = \emptyset$
56	52 53 55	syl2anc	$⊢ Lim x \to \emptyset ↑_{𝑜} x = \emptyset$
57		0ss	$⊢ \emptyset \subseteq B ↑_{𝑜} x$
58	56 57	eqsstrdi	$⊢ Lim x \to \emptyset ↑_{𝑜} x \subseteq B ↑_{𝑜} x$
59		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} x = \emptyset ↑_{𝑜} x$
60	59	sseq1d	$⊢ A = \emptyset \to (A ↑_{𝑜} x \subseteq B ↑_{𝑜} x \leftrightarrow \emptyset ↑_{𝑜} x \subseteq B ↑_{𝑜} x)$
61	58 60	syl5ibr	$⊢ A = \emptyset \to (Lim x \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x)$
62	61	adantl	$⊢ ((B \in On \land A \in B) \land A = \emptyset) \to (Lim x \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x)$
63	62	a1dd	$⊢ ((B \in On \land A \in B) \land A = \emptyset) \to (Lim x \to (\forall y \in x A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x))$
64		ss2iun	$⊢ \forall y \in x A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to ⋃_{y \in x} (A ↑_{𝑜} y) \subseteq ⋃_{y \in x} (B ↑_{𝑜} y)$
65		oelim	$⊢ ((A \in On \land (x \in V \land Lim x)) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
66	50 65	mpanlr1	$⊢ ((A \in On \land Lim x) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
67	66	an32s	$⊢ ((A \in On \land \emptyset \in A) \land Lim x) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
68	67	adantllr	$⊢ (((A \in On \land (B \in On \land A \in B)) \land \emptyset \in A) \land Lim x) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
69	21	anim1i	$⊢ ((B \in On \land A \in B) \land Lim x) \to (B \in On \land Lim x)$
70		ne0i	$⊢ A \in B \to B \neq \emptyset$
71		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
72	70 71	syl5ibr	$⊢ B \in On \to (A \in B \to \emptyset \in B)$
73	72	imp	$⊢ (B \in On \land A \in B) \to \emptyset \in B$
74	73	adantr	$⊢ ((B \in On \land A \in B) \land Lim x) \to \emptyset \in B$
75		oelim	$⊢ ((B \in On \land (x \in V \land Lim x)) \land \emptyset \in B) \to B ↑_{𝑜} x = ⋃_{y \in x} (B ↑_{𝑜} y)$
76	50 75	mpanlr1	$⊢ ((B \in On \land Lim x) \land \emptyset \in B) \to B ↑_{𝑜} x = ⋃_{y \in x} (B ↑_{𝑜} y)$
77	69 74 76	syl2anc	$⊢ ((B \in On \land A \in B) \land Lim x) \to B ↑_{𝑜} x = ⋃_{y \in x} (B ↑_{𝑜} y)$
78	77	ad4ant24	$⊢ (((A \in On \land (B \in On \land A \in B)) \land \emptyset \in A) \land Lim x) \to B ↑_{𝑜} x = ⋃_{y \in x} (B ↑_{𝑜} y)$
79	68 78	sseq12d	$⊢ (((A \in On \land (B \in On \land A \in B)) \land \emptyset \in A) \land Lim x) \to (A ↑_{𝑜} x \subseteq B ↑_{𝑜} x \leftrightarrow ⋃_{y \in x} (A ↑_{𝑜} y) \subseteq ⋃_{y \in x} (B ↑_{𝑜} y))$
80	64 79	syl5ibr	$⊢ (((A \in On \land (B \in On \land A \in B)) \land \emptyset \in A) \land Lim x) \to (\forall y \in x A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x)$
81	80	ex	$⊢ ((A \in On \land (B \in On \land A \in B)) \land \emptyset \in A) \to (Lim x \to (\forall y \in x A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x))$
82	63 81	oe0lem	$⊢ (A \in On \land (B \in On \land A \in B)) \to (Lim x \to (\forall y \in x A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x))$
83	13	ancri	$⊢ (B \in On \land A \in B) \to (A \in On \land (B \in On \land A \in B))$
84	82 83	syl11	$⊢ Lim x \to ((B \in On \land A \in B) \to (\forall y \in x A ↑_{𝑜} y \subseteq B ↑_{𝑜} y \to A ↑_{𝑜} x \subseteq B ↑_{𝑜} x))$
85	3 6 9 12 20 49 84	tfinds3	$⊢ C \in On \to ((B \in On \land A \in B) \to A ↑_{𝑜} C \subseteq B ↑_{𝑜} C)$
86	85	expd	$⊢ C \in On \to (B \in On \to (A \in B \to A ↑_{𝑜} C \subseteq B ↑_{𝑜} C))$
87	86	impcom	$⊢ (B \in On \land C \in On) \to (A \in B \to A ↑_{𝑜} C \subseteq B ↑_{𝑜} C)$

Metamath Proof Explorer

Theorem oewordri

Proof