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 43236

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 6405	. . . 4 ⊢ (𝐵 ∈ On → Ord 𝐵)
2		orduniorsuc 7866	. . . . 5 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵))
3		unizlim 6518	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
4	3	biimpd 229	. . . . . 6 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
5	4	orim1d 966	. . . . 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 7456	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ ∅))
10		onov0suclim.0	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)
11	9, 10	sylan9eqr 2802	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ⊗ 𝐵) = 𝐷)
12	11	ex 412	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
13	12	ad2antrr 725	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
14		eloni 6405	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
15		0elsuc 7871	. . . . . . . . . . . . 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 2847	. . . . . . . . . 10 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ 𝐵)
20		n0i 4363	. . . . . . . . . 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 6454	. . . . . . . . 9 ⊢ ¬ Lim ∅
26		limeq 6407	. . . . . . . . 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 1128	. . . . 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 6407	. . . . . . . . . . . 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 7879	. . . . . . . . . 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 1128	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
46	45	ex 412	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
47	31, 46	jaod 858	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
48		1n0 8544	. . . . . . . . 9 ⊢ 1_o ≠ ∅
49		necom 3000	. . . . . . . . . . 11 ⊢ (1_o ≠ ∅ ↔ ∅ ≠ 1_o)
50		df-1o 8522	. . . . . . . . . . . . 13 ⊢ 1_o = suc ∅
51		uni0 4959	. . . . . . . . . . . . . 14 ⊢ ∪ ∅ = ∅
52		suceq 6461	. . . . . . . . . . . . . 14 ⊢ (∪ ∅ = ∅ → suc ∪ ∅ = suc ∅)
53	51, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ suc ∪ ∅ = suc ∅
54	50, 53	eqtr4i 2771	. . . . . . . . . . . 12 ⊢ 1_o = suc ∪ ∅
55	54	neeq2i 3012	. . . . . . . . . . 11 ⊢ (∅ ≠ 1_o ↔ ∅ ≠ suc ∪ ∅)
56		df-ne 2947	. . . . . . . . . . 11 ⊢ (∅ ≠ suc ∪ ∅ ↔ ¬ ∅ = suc ∪ ∅)
57	49, 55, 56	3bitri 297	. . . . . . . . . 10 ⊢ (1_o ≠ ∅ ↔ ¬ ∅ = suc ∪ ∅)
58		id 22	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → 𝐵 = ∅)
59		unieq 4942	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → ∪ 𝐵 = ∪ ∅)
60		suceq 6461	. . . . . . . . . . . . 13 ⊢ (∪ 𝐵 = ∪ ∅ → suc ∪ 𝐵 = suc ∪ ∅)
61	59, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → suc ∪ 𝐵 = suc ∪ ∅)
62	58, 61	eqeq12d 2756	. . . . . . . . . . 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 770	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → 𝐵 = suc 𝐶)
70	69	oveq2d 7464	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ suc 𝐶))
71		onov0suclim.suc	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)
72	71	adantrl 715	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ suc 𝐶) = 𝐸)
73	70, 72	eqtrd 2780	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = 𝐸)
74	73	ex 412	. . . . . 6 ⊢ (𝐴 ∈ On → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
75	74	ad2antrr 725	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
76		onuni 7824	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ∪ 𝐵 ∈ On)
77		nlimsucg 7879	. . . . . . . . 9 ⊢ (∪ 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
78	76, 77	syl 17	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
79		limeq 6407	. . . . . . . . . 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 713	. . . . . 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 412	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc ∪ 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
87	47, 86	jaod 858	. 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 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∅c0 4352 ∪ cuni 4931 Ord word 6394 Oncon0 6395 Lim wlim 6396 suc csuc 6397 (class class class)co 7448 1_oc1o 8515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-11 2158 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-tr 5284 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fv 6581 df-ov 7451 df-1o 8522

This theorem is referenced by: oa0suclim 43237 om0suclim 43238 oe0suclim 43239

W3C validator