onov0suclim - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > onov0suclim		Structured version Visualization version GIF version

Theorem onov0suclim 41795

Description: Compactly express rules for binary operations on ordinals. (Contributed by RP, 18-Jan-2025.)

**Hypotheses**
Ref	Expression
onov0suclim.0	⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)
onov0suclim.suc	⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)
onov0suclim.lim	⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 ⊗ 𝐵) = 𝐹)

**Assertion**
Ref	Expression
onov0suclim	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))

**Proof of Theorem onov0suclim**
Step	Hyp	Ref	Expression
1		eloni 6363	. . . 4 ⊢ (𝐵 ∈ On → Ord 𝐵)
2		orduniorsuc 7801	. . . . 5 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵))
3		unizlim 6476	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
4	3	biimpd 228	. . . . . 6 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
5	4	orim1d 964	. . . . 5 ⊢ (Ord 𝐵 → ((𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵)))
6	2, 5	mpd 15	. . . 4 ⊢ (Ord 𝐵 → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
7	1, 6	syl 17	. . 3 ⊢ (𝐵 ∈ On → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
8	7	adantl 482	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
9		oveq2 7401	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ ∅))
10		onov0suclim.0	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)
11	9, 10	sylan9eqr 2793	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ⊗ 𝐵) = 𝐷)
12	11	ex 413	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
13	12	ad2antrr 724	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
14		eloni 6363	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
15		0elsuc 7806	. . . . . . . . . . . . 13 ⊢ (Ord 𝐶 → ∅ ∈ suc 𝐶)
16	14, 15	syl 17	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ On → ∅ ∈ suc 𝐶)
17	16	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → 𝐵 = suc 𝐶)
19	17, 18	eleqtrrd 2835	. . . . . . . . . 10 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ 𝐵)
20		n0i 4329	. . . . . . . . . 10 ⊢ (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
21	19, 20	syl 17	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ 𝐵 = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
23	22	adantl 482	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
24	23	impancom 452	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
25		nlim0 6412	. . . . . . . . 9 ⊢ ¬ Lim ∅
26		limeq 6365	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
27	25, 26	mtbiri 326	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ Lim 𝐵)
28	27	adantl 482	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
29	28	pm2.21d 121	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
30	13, 24, 29	3jca 1128	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
31	30	ex 413	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
32	27	con2i 139	. . . . . . . 8 ⊢ (Lim 𝐵 → ¬ 𝐵 = ∅)
33	32	adantl 482	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ¬ 𝐵 = ∅)
34	33	pm2.21d 121	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
35		limeq 6365	. . . . . . . . . . . 12 ⊢ (𝐵 = suc 𝐶 → (Lim 𝐵 ↔ Lim suc 𝐶))
36	35	notbid 317	. . . . . . . . . . 11 ⊢ (𝐵 = suc 𝐶 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶))
37	36	biimprd 247	. . . . . . . . . 10 ⊢ (𝐵 = suc 𝐶 → (¬ Lim suc 𝐶 → ¬ Lim 𝐵))
38		nlimsucg 7814	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → ¬ Lim suc 𝐶)
39	37, 38	impel 506	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ Lim 𝐵)
40	39	adantl 482	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → ¬ Lim 𝐵)
41	40	pm2.21d 121	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐸))
42	41	impancom 452	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
43		onov0suclim.lim	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 ⊗ 𝐵) = 𝐹)
44	43	a1d 25	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
45	34, 42, 44	3jca 1128	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
46	45	ex 413	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
47	31, 46	jaod 857	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
48		1n0 8470	. . . . . . . . 9 ⊢ 1_o ≠ ∅
49		necom 2993	. . . . . . . . . . 11 ⊢ (1_o ≠ ∅ ↔ ∅ ≠ 1_o)
50		df-1o 8448	. . . . . . . . . . . . 13 ⊢ 1_o = suc ∅
51		uni0 4932	. . . . . . . . . . . . . 14 ⊢ ∪ ∅ = ∅
52		suceq 6419	. . . . . . . . . . . . . 14 ⊢ (∪ ∅ = ∅ → suc ∪ ∅ = suc ∅)
53	51, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ suc ∪ ∅ = suc ∅
54	50, 53	eqtr4i 2762	. . . . . . . . . . . 12 ⊢ 1_o = suc ∪ ∅
55	54	neeq2i 3005	. . . . . . . . . . 11 ⊢ (∅ ≠ 1_o ↔ ∅ ≠ suc ∪ ∅)
56		df-ne 2940	. . . . . . . . . . 11 ⊢ (∅ ≠ suc ∪ ∅ ↔ ¬ ∅ = suc ∪ ∅)
57	49, 55, 56	3bitri 296	. . . . . . . . . 10 ⊢ (1_o ≠ ∅ ↔ ¬ ∅ = suc ∪ ∅)
58		id 22	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → 𝐵 = ∅)
59		unieq 4912	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → ∪ 𝐵 = ∪ ∅)
60		suceq 6419	. . . . . . . . . . . . 13 ⊢ (∪ 𝐵 = ∪ ∅ → suc ∪ 𝐵 = suc ∪ ∅)
61	59, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → suc ∪ 𝐵 = suc ∪ ∅)
62	58, 61	eqeq12d 2747	. . . . . . . . . . 11 ⊢ (𝐵 = ∅ → (𝐵 = suc ∪ 𝐵 ↔ ∅ = suc ∪ ∅))
63	62	notbid 317	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → (¬ 𝐵 = suc ∪ 𝐵 ↔ ¬ ∅ = suc ∪ ∅))
64	57, 63	bitr4id 289	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (1_o ≠ ∅ ↔ ¬ 𝐵 = suc ∪ 𝐵))
65	48, 64	mpbii 232	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ 𝐵 = suc ∪ 𝐵)
66	65	con2i 139	. . . . . . 7 ⊢ (𝐵 = suc ∪ 𝐵 → ¬ 𝐵 = ∅)
67	66	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ 𝐵 = ∅)
68	67	pm2.21d 121	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
69		simprl 769	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → 𝐵 = suc 𝐶)
70	69	oveq2d 7409	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ suc 𝐶))
71		onov0suclim.suc	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)
72	71	adantrl 714	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ suc 𝐶) = 𝐸)
73	70, 72	eqtrd 2771	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = 𝐸)
74	73	ex 413	. . . . . 6 ⊢ (𝐴 ∈ On → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
75	74	ad2antrr 724	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
76		onuni 7759	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ∪ 𝐵 ∈ On)
77		nlimsucg 7814	. . . . . . . . 9 ⊢ (∪ 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
78	76, 77	syl 17	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
79		limeq 6365	. . . . . . . . . 10 ⊢ (𝐵 = suc ∪ 𝐵 → (Lim 𝐵 ↔ Lim suc ∪ 𝐵))
80	79	notbid 317	. . . . . . . . 9 ⊢ (𝐵 = suc ∪ 𝐵 → (¬ Lim 𝐵 ↔ ¬ Lim suc ∪ 𝐵))
81	80	biimprd 247	. . . . . . . 8 ⊢ (𝐵 = suc ∪ 𝐵 → (¬ Lim suc ∪ 𝐵 → ¬ Lim 𝐵))
82	78, 81	mpan9 507	. . . . . . 7 ⊢ ((𝐵 ∈ On ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
83	82	adantll 712	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
84	83	pm2.21d 121	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
85	68, 75, 84	3jca 1128	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
86	85	ex 413	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc ∪ 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
87	47, 86	jaod 857	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
88	8, 87	mpd 15	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2939 ∅c0 4318 ∪ cuni 4901 Ord word 6352 Oncon0 6353 Lim wlim 6354 suc csuc 6355 (class class class)co 7393 1_oc1o 8441

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 ax-un 7708

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-opab 5204 df-tr 5259 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fv 6540 df-ov 7396 df-1o 8448

This theorem is referenced by: oa0suclim 41796 om0suclim 41797 oe0suclim 41798

W3C validator