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 43635

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 6335	. . . 4 ⊢ (𝐵 ∈ On → Ord 𝐵)
2		orduniorsuc 7782	. . . . 5 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵))
3		unizlim 6449	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
4	3	biimpd 229	. . . . . 6 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
5	4	orim1d 968	. . . . 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 481	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
9		oveq2 7376	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ ∅))
10		onov0suclim.0	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)
11	9, 10	sylan9eqr 2794	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ⊗ 𝐵) = 𝐷)
12	11	ex 412	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
13	12	ad2antrr 727	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
14		eloni 6335	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
15		0elsuc 7787	. . . . . . . . . . . . 13 ⊢ (Ord 𝐶 → ∅ ∈ suc 𝐶)
16	14, 15	syl 17	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ On → ∅ ∈ suc 𝐶)
17	16	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → 𝐵 = suc 𝐶)
19	17, 18	eleqtrrd 2840	. . . . . . . . . 10 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ 𝐵)
20		n0i 4294	. . . . . . . . . 10 ⊢ (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
21	19, 20	syl 17	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ 𝐵 = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
23	22	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
24	23	impancom 451	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
25		nlim0 6385	. . . . . . . . 9 ⊢ ¬ Lim ∅
26		limeq 6337	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
27	25, 26	mtbiri 327	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ Lim 𝐵)
28	27	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
29	28	pm2.21d 121	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
30	13, 24, 29	3jca 1129	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
31	30	ex 412	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
32	27	con2i 139	. . . . . . . 8 ⊢ (Lim 𝐵 → ¬ 𝐵 = ∅)
33	32	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ¬ 𝐵 = ∅)
34	33	pm2.21d 121	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
35		limeq 6337	. . . . . . . . . . . 12 ⊢ (𝐵 = suc 𝐶 → (Lim 𝐵 ↔ Lim suc 𝐶))
36	35	notbid 318	. . . . . . . . . . 11 ⊢ (𝐵 = suc 𝐶 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶))
37	36	biimprd 248	. . . . . . . . . 10 ⊢ (𝐵 = suc 𝐶 → (¬ Lim suc 𝐶 → ¬ Lim 𝐵))
38		nlimsucg 7794	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → ¬ Lim suc 𝐶)
39	37, 38	impel 505	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ Lim 𝐵)
40	39	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → ¬ Lim 𝐵)
41	40	pm2.21d 121	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐸))
42	41	impancom 451	. . . . . 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 1129	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
46	45	ex 412	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
47	31, 46	jaod 860	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
48		1n0 8425	. . . . . . . . 9 ⊢ 1_o ≠ ∅
49		necom 2986	. . . . . . . . . . 11 ⊢ (1_o ≠ ∅ ↔ ∅ ≠ 1_o)
50		df-1o 8407	. . . . . . . . . . . . 13 ⊢ 1_o = suc ∅
51		uni0 4893	. . . . . . . . . . . . . 14 ⊢ ∪ ∅ = ∅
52		suceq 6393	. . . . . . . . . . . . . 14 ⊢ (∪ ∅ = ∅ → suc ∪ ∅ = suc ∅)
53	51, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ suc ∪ ∅ = suc ∅
54	50, 53	eqtr4i 2763	. . . . . . . . . . . 12 ⊢ 1_o = suc ∪ ∅
55	54	neeq2i 2998	. . . . . . . . . . 11 ⊢ (∅ ≠ 1_o ↔ ∅ ≠ suc ∪ ∅)
56		df-ne 2934	. . . . . . . . . . 11 ⊢ (∅ ≠ suc ∪ ∅ ↔ ¬ ∅ = suc ∪ ∅)
57	49, 55, 56	3bitri 297	. . . . . . . . . 10 ⊢ (1_o ≠ ∅ ↔ ¬ ∅ = suc ∪ ∅)
58		id 22	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → 𝐵 = ∅)
59		unieq 4876	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → ∪ 𝐵 = ∪ ∅)
60		suceq 6393	. . . . . . . . . . . . 13 ⊢ (∪ 𝐵 = ∪ ∅ → suc ∪ 𝐵 = suc ∪ ∅)
61	59, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → suc ∪ 𝐵 = suc ∪ ∅)
62	58, 61	eqeq12d 2753	. . . . . . . . . . 11 ⊢ (𝐵 = ∅ → (𝐵 = suc ∪ 𝐵 ↔ ∅ = suc ∪ ∅))
63	62	notbid 318	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → (¬ 𝐵 = suc ∪ 𝐵 ↔ ¬ ∅ = suc ∪ ∅))
64	57, 63	bitr4id 290	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (1_o ≠ ∅ ↔ ¬ 𝐵 = suc ∪ 𝐵))
65	48, 64	mpbii 233	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ 𝐵 = suc ∪ 𝐵)
66	65	con2i 139	. . . . . . 7 ⊢ (𝐵 = suc ∪ 𝐵 → ¬ 𝐵 = ∅)
67	66	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ 𝐵 = ∅)
68	67	pm2.21d 121	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
69		simprl 771	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → 𝐵 = suc 𝐶)
70	69	oveq2d 7384	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ suc 𝐶))
71		onov0suclim.suc	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)
72	71	adantrl 717	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ suc 𝐶) = 𝐸)
73	70, 72	eqtrd 2772	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = 𝐸)
74	73	ex 412	. . . . . 6 ⊢ (𝐴 ∈ On → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
75	74	ad2antrr 727	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
76		onuni 7743	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ∪ 𝐵 ∈ On)
77		nlimsucg 7794	. . . . . . . . 9 ⊢ (∪ 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
78	76, 77	syl 17	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
79		limeq 6337	. . . . . . . . . 10 ⊢ (𝐵 = suc ∪ 𝐵 → (Lim 𝐵 ↔ Lim suc ∪ 𝐵))
80	79	notbid 318	. . . . . . . . 9 ⊢ (𝐵 = suc ∪ 𝐵 → (¬ Lim 𝐵 ↔ ¬ Lim suc ∪ 𝐵))
81	80	biimprd 248	. . . . . . . 8 ⊢ (𝐵 = suc ∪ 𝐵 → (¬ Lim suc ∪ 𝐵 → ¬ Lim 𝐵))
82	78, 81	mpan9 506	. . . . . . 7 ⊢ ((𝐵 ∈ On ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
83	82	adantll 715	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
84	83	pm2.21d 121	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
85	68, 75, 84	3jca 1129	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
86	85	ex 412	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc ∪ 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
87	47, 86	jaod 860	. 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 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∅c0 4287 ∪ cuni 4865 Ord word 6324 Oncon0 6325 Lim wlim 6326 suc csuc 6327 (class class class)co 7368 1_oc1o 8400

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-tr 5208 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fv 6508 df-ov 7371 df-1o 8407

This theorem is referenced by: oa0suclim 43636 om0suclim 43637 oe0suclim 43638

W3C validator