oen0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > oen0		Structured version Visualization version GIF version

Theorem oen0 8601

Description: Ordinal exponentiation with a nonzero base is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67. (Contributed by NM, 4-Jan-2005.)

**Assertion**
Ref	Expression
oen0	⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o 𝐵))

Proof of Theorem oen0 Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7423	. . . . . 6 ⊢ (𝑥 = ∅ → (𝐴 ↑_o 𝑥) = (𝐴 ↑_o ∅))
2	1	eleq2d 2815	. . . . 5 ⊢ (𝑥 = ∅ → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ ∅ ∈ (𝐴 ↑_o ∅)))
3		oveq2 7423	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ↑_o 𝑥) = (𝐴 ↑_o 𝑦))
4	3	eleq2d 2815	. . . . 5 ⊢ (𝑥 = 𝑦 → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ ∅ ∈ (𝐴 ↑_o 𝑦)))
5		oveq2 7423	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝐴 ↑_o 𝑥) = (𝐴 ↑_o suc 𝑦))
6	5	eleq2d 2815	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ ∅ ∈ (𝐴 ↑_o suc 𝑦)))
7		oveq2 7423	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝐴 ↑_o 𝑥) = (𝐴 ↑_o 𝐵))
8	7	eleq2d 2815	. . . . 5 ⊢ (𝑥 = 𝐵 → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ ∅ ∈ (𝐴 ↑_o 𝐵)))
9		0lt1o 8519	. . . . . . 7 ⊢ ∅ ∈ 1_o
10		oe0 8537	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝐴 ↑_o ∅) = 1_o)
11	9, 10	eleqtrrid 2836	. . . . . 6 ⊢ (𝐴 ∈ On → ∅ ∈ (𝐴 ↑_o ∅))
12	11	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o ∅))
13		oecl 8552	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑_o 𝑦) ∈ On)
14		omordi 8581	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ (𝐴 ↑_o 𝑦) ∈ On) ∧ ∅ ∈ (𝐴 ↑_o 𝑦)) → (∅ ∈ 𝐴 → ((𝐴 ↑_o 𝑦) ·_o ∅) ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
15		om0 8532	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↑_o 𝑦) ∈ On → ((𝐴 ↑_o 𝑦) ·_o ∅) = ∅)
16	15	eleq1d 2814	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↑_o 𝑦) ∈ On → (((𝐴 ↑_o 𝑦) ·_o ∅) ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴) ↔ ∅ ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
17	16	ad2antlr 726	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ (𝐴 ↑_o 𝑦) ∈ On) ∧ ∅ ∈ (𝐴 ↑_o 𝑦)) → (((𝐴 ↑_o 𝑦) ·_o ∅) ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴) ↔ ∅ ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
18	14, 17	sylibd 238	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ On ∧ (𝐴 ↑_o 𝑦) ∈ On) ∧ ∅ ∈ (𝐴 ↑_o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
19	13, 18	syldanl 601	. . . . . . . . . 10 ⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ (𝐴 ↑_o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
20		oesuc 8542	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑_o suc 𝑦) = ((𝐴 ↑_o 𝑦) ·_o 𝐴))
21	20	eleq2d 2815	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (∅ ∈ (𝐴 ↑_o suc 𝑦) ↔ ∅ ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
22	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ (𝐴 ↑_o 𝑦)) → (∅ ∈ (𝐴 ↑_o suc 𝑦) ↔ ∅ ∈ ((𝐴 ↑_o 𝑦) ·_o 𝐴)))
23	19, 22	sylibrd 259	. . . . . . . . 9 ⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ (𝐴 ↑_o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑_o suc 𝑦)))
24	23	exp31 419	. . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑦 ∈ On → (∅ ∈ (𝐴 ↑_o 𝑦) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑_o suc 𝑦)))))
25	24	com12 32	. . . . . . 7 ⊢ (𝑦 ∈ On → (𝐴 ∈ On → (∅ ∈ (𝐴 ↑_o 𝑦) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑_o suc 𝑦)))))
26	25	com34 91	. . . . . 6 ⊢ (𝑦 ∈ On → (𝐴 ∈ On → (∅ ∈ 𝐴 → (∅ ∈ (𝐴 ↑_o 𝑦) → ∅ ∈ (𝐴 ↑_o suc 𝑦)))))
27	26	impd 410	. . . . 5 ⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (∅ ∈ (𝐴 ↑_o 𝑦) → ∅ ∈ (𝐴 ↑_o suc 𝑦))))
28		0ellim 6427	. . . . . . . . . . . 12 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
29		eqimss2 4038	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↑_o ∅) = 1_o → 1_o ⊆ (𝐴 ↑_o ∅))
30	10, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → 1_o ⊆ (𝐴 ↑_o ∅))
31		oveq2 7423	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (𝐴 ↑_o 𝑦) = (𝐴 ↑_o ∅))
32	31	sseq2d 4011	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → (1_o ⊆ (𝐴 ↑_o 𝑦) ↔ 1_o ⊆ (𝐴 ↑_o ∅)))
33	32	rspcev 3608	. . . . . . . . . . . 12 ⊢ ((∅ ∈ 𝑥 ∧ 1_o ⊆ (𝐴 ↑_o ∅)) → ∃𝑦 ∈ 𝑥 1_o ⊆ (𝐴 ↑_o 𝑦))
34	28, 30, 33	syl2an 595	. . . . . . . . . . 11 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → ∃𝑦 ∈ 𝑥 1_o ⊆ (𝐴 ↑_o 𝑦))
35		ssiun 5044	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 1_o ⊆ (𝐴 ↑_o 𝑦) → 1_o ⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → 1_o ⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
37	36	adantrr 716	. . . . . . . . 9 ⊢ ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1_o ⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
38		vex 3474	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
39		oelim 8549	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑_o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
40	38, 39	mpanlr1 705	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑_o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
41	40	anasss 466	. . . . . . . . . 10 ⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴 ↑_o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
42	41	an12s 648	. . . . . . . . 9 ⊢ ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴 ↑_o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑_o 𝑦))
43	37, 42	sseqtrrd 4020	. . . . . . . 8 ⊢ ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1_o ⊆ (𝐴 ↑_o 𝑥))
44		limelon 6428	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
45	38, 44	mpan 689	. . . . . . . . . . 11 ⊢ (Lim 𝑥 → 𝑥 ∈ On)
46		oecl 8552	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ↑_o 𝑥) ∈ On)
47	46	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ↑_o 𝑥) ∈ On)
48	45, 47	sylan 579	. . . . . . . . . 10 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (𝐴 ↑_o 𝑥) ∈ On)
49		eloni 6374	. . . . . . . . . 10 ⊢ ((𝐴 ↑_o 𝑥) ∈ On → Ord (𝐴 ↑_o 𝑥))
50		ordgt0ge1 8508	. . . . . . . . . 10 ⊢ (Ord (𝐴 ↑_o 𝑥) → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ 1_o ⊆ (𝐴 ↑_o 𝑥)))
51	48, 49, 50	3syl 18	. . . . . . . . 9 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ 1_o ⊆ (𝐴 ↑_o 𝑥)))
52	51	adantrr 716	. . . . . . . 8 ⊢ ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∅ ∈ (𝐴 ↑_o 𝑥) ↔ 1_o ⊆ (𝐴 ↑_o 𝑥)))
53	43, 52	mpbird 257	. . . . . . 7 ⊢ ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ∅ ∈ (𝐴 ↑_o 𝑥))
54	53	ex 412	. . . . . 6 ⊢ (Lim 𝑥 → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o 𝑥)))
55	54	a1dd 50	. . . . 5 ⊢ (Lim 𝑥 → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (∀𝑦 ∈ 𝑥 ∅ ∈ (𝐴 ↑_o 𝑦) → ∅ ∈ (𝐴 ↑_o 𝑥))))
56	2, 4, 6, 8, 12, 27, 55	tfinds3 7864	. . . 4 ⊢ (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o 𝐵)))
57	56	expd 415	. . 3 ⊢ (𝐵 ∈ On → (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑_o 𝐵))))
58	57	com12 32	. 2 ⊢ (𝐴 ∈ On → (𝐵 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑_o 𝐵))))
59	58	imp31 417	1 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ∀wral 3057 ∃wrex 3066 Vcvv 3470 ⊆ wss 3945 ∅c0 4319 ∪ ciun 4992 Ord word 6363 Oncon0 6364 Lim wlim 6365 suc csuc 6366 (class class class)co 7415 1_oc1o 8474 ·_o comu 8479 ↑_o coe 8480

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pr 5424 ax-un 7735

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-ral 3058 df-rex 3067 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4905 df-iun 4994 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7866 df-2nd 7989 df-frecs 8281 df-wrecs 8312 df-recs 8386 df-rdg 8425 df-1o 8481 df-oadd 8485 df-omul 8486 df-oexp 8487

This theorem is referenced by: oeordi 8602 oeordsuc 8609 oeoelem 8613 oelimcl 8615 oeeui 8617 cantnflt 9690 cnfcom 9718 infxpenc 10036 infxpenc2 10040 onexoegt 42663 cantnftermord 42740 oacl2g 42750 onmcl 42751 omabs2 42752 omcl2 42753 ofoaf 42775 ofoafo 42776

W3C validator

	
		OSZAR »