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 44118

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 6367	. . . 4 ⊢ (𝐵 ∈ On → Ord 𝐵)
2		orduniorsuc 7827	. . . . 5 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵))
3		unizlim 6482	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
4	3	biimpd 232	. . . . . 6 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
5	4	orim1d 981	. . . . 5 ⊢ (Ord 𝐵 → ((𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵)))
6	2, 5	mpd 16	. . . 4 ⊢ (Ord 𝐵 → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
7	1, 6	syl 18	. . 3 ⊢ (𝐵 ∈ On → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
8	7	adantl 487	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
9		oveq2 7422	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ ∅))
10		onov0suclim.0	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)
11	9, 10	sylan9eqr 2817	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ⊗ 𝐵) = 𝐷)
12	11	ex 418	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
13	12	ad2antrr 739	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
14		eloni 6367	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
15		0elsuc 7832	. . . . . . . . . . . . 13 ⊢ (Ord 𝐶 → ∅ ∈ suc 𝐶)
16	14, 15	syl 18	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ On → ∅ ∈ suc 𝐶)
17	16	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18		simpl 488	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → 𝐵 = suc 𝐶)
19	17, 18	eleqtrrd 2863	. . . . . . . . . 10 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ 𝐵)
20		n0i 4286	. . . . . . . . . 10 ⊢ (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
21	19, 20	syl 18	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ 𝐵 = ∅)
22	21	pm2.21d 122	. . . . . . . 8 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
23	22	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
24	23	impancom 457	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
25		nlim0 6418	. . . . . . . . 9 ⊢ ¬ Lim ∅
26		limeq 6369	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
27	25, 26	mtbiri 330	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ Lim 𝐵)
28	27	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
29	28	pm2.21d 122	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
30	13, 24, 29	3jca 1146	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
31	30	ex 418	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
32	27	con2i 140	. . . . . . . 8 ⊢ (Lim 𝐵 → ¬ 𝐵 = ∅)
33	32	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ¬ 𝐵 = ∅)
34	33	pm2.21d 122	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
35		limeq 6369	. . . . . . . . . . . 12 ⊢ (𝐵 = suc 𝐶 → (Lim 𝐵 ↔ Lim suc 𝐶))
36	35	notbid 321	. . . . . . . . . . 11 ⊢ (𝐵 = suc 𝐶 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶))
37	36	biimprd 251	. . . . . . . . . 10 ⊢ (𝐵 = suc 𝐶 → (¬ Lim suc 𝐶 → ¬ Lim 𝐵))
38		nlimsucg 7839	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → ¬ Lim suc 𝐶)
39	37, 38	impel 515	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ Lim 𝐵)
40	39	adantl 487	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → ¬ Lim 𝐵)
41	40	pm2.21d 122	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐸))
42	41	impancom 457	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
43		onov0suclim.lim	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 ⊗ 𝐵) = 𝐹)
44	43	a1d 26	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
45	34, 42, 44	3jca 1146	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
46	45	ex 418	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
47	31, 46	jaod 873	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
48		1n0 8477	. . . . . . . . 9 ⊢ 1_o ≠ ∅
49		necom 3008	. . . . . . . . . . 11 ⊢ (1_o ≠ ∅ ↔ ∅ ≠ 1_o)
50		df-1o 8458	. . . . . . . . . . . . 13 ⊢ 1_o = suc ∅
51		uni0 4896	. . . . . . . . . . . . . 14 ⊢ ∪ ∅ = ∅
52		suceq 6426	. . . . . . . . . . . . . 14 ⊢ (∪ ∅ = ∅ → suc ∪ ∅ = suc ∅)
53	51, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ suc ∪ ∅ = suc ∅
54	50, 53	eqtr4i 2786	. . . . . . . . . . . 12 ⊢ 1_o = suc ∪ ∅
55	54	neeq2i 3020	. . . . . . . . . . 11 ⊢ (∅ ≠ 1_o ↔ ∅ ≠ suc ∪ ∅)
56		df-ne 2956	. . . . . . . . . . 11 ⊢ (∅ ≠ suc ∪ ∅ ↔ ¬ ∅ = suc ∪ ∅)
57	49, 55, 56	3bitri 300	. . . . . . . . . 10 ⊢ (1_o ≠ ∅ ↔ ¬ ∅ = suc ∪ ∅)
58		id 23	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → 𝐵 = ∅)
59		unieq 4878	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → ∪ 𝐵 = ∪ ∅)
60		suceq 6426	. . . . . . . . . . . . 13 ⊢ (∪ 𝐵 = ∪ ∅ → suc ∪ 𝐵 = suc ∪ ∅)
61	59, 60	syl 18	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → suc ∪ 𝐵 = suc ∪ ∅)
62	58, 61	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝐵 = ∅ → (𝐵 = suc ∪ 𝐵 ↔ ∅ = suc ∪ ∅))
63	62	notbid 321	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → (¬ 𝐵 = suc ∪ 𝐵 ↔ ¬ ∅ = suc ∪ ∅))
64	57, 63	bitr4id 293	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (1_o ≠ ∅ ↔ ¬ 𝐵 = suc ∪ 𝐵))
65	48, 64	mpbii 236	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ 𝐵 = suc ∪ 𝐵)
66	65	con2i 140	. . . . . . 7 ⊢ (𝐵 = suc ∪ 𝐵 → ¬ 𝐵 = ∅)
67	66	adantl 487	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ 𝐵 = ∅)
68	67	pm2.21d 122	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
69		simprl 783	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → 𝐵 = suc 𝐶)
70	69	oveq2d 7430	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ suc 𝐶))
71		onov0suclim.suc	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)
72	71	adantrl 729	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ suc 𝐶) = 𝐸)
73	70, 72	eqtrd 2795	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = 𝐸)
74	73	ex 418	. . . . . 6 ⊢ (𝐴 ∈ On → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
75	74	ad2antrr 739	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
76		onuni 7788	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ∪ 𝐵 ∈ On)
77		nlimsucg 7839	. . . . . . . . 9 ⊢ (∪ 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
78	76, 77	syl 18	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
79		limeq 6369	. . . . . . . . . 10 ⊢ (𝐵 = suc ∪ 𝐵 → (Lim 𝐵 ↔ Lim suc ∪ 𝐵))
80	79	notbid 321	. . . . . . . . 9 ⊢ (𝐵 = suc ∪ 𝐵 → (¬ Lim 𝐵 ↔ ¬ Lim suc ∪ 𝐵))
81	80	biimprd 251	. . . . . . . 8 ⊢ (𝐵 = suc ∪ 𝐵 → (¬ Lim suc ∪ 𝐵 → ¬ Lim 𝐵))
82	78, 81	mpan9 516	. . . . . . 7 ⊢ ((𝐵 ∈ On ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
83	82	adantll 727	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
84	83	pm2.21d 122	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
85	68, 75, 84	3jca 1146	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
86	85	ex 418	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc ∪ 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
87	47, 86	jaod 873	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
88	8, 87	mpd 16	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∅c0 4279 ∪ cuni 4867 Ord word 6356 Oncon0 6357 Lim wlim 6358 suc csuc 6359 (class class class)co 7414 1_oc1o 8451

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pr 5398 ax-un 7737

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-tr 5213 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fv 6541 df-ov 7417 df-1o 8458

This theorem is used by: oa0suclim 44119 om0suclim 44120 oe0suclim 44121

W3C validator