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 43893

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 6371	. . . 4 ⊢ (𝐵 ∈ On → Ord 𝐵)
2		orduniorsuc 7826	. . . . 5 ⊢ (Ord 𝐵 → (𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵))
3		unizlim 6486	. . . . . . 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 486	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc ∪ 𝐵))
9		oveq2 7419	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ ∅))
10		onov0suclim.0	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)
11	9, 10	sylan9eqr 2826	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ⊗ 𝐵) = 𝐷)
12	11	ex 417	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
13	12	ad2antrr 738	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
14		eloni 6371	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
15		0elsuc 7831	. . . . . . . . . . . . 13 ⊢ (Ord 𝐶 → ∅ ∈ suc 𝐶)
16	14, 15	syl 18	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ On → ∅ ∈ suc 𝐶)
17	16	adantl 486	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18		simpl 487	. . . . . . . . . . 11 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → 𝐵 = suc 𝐶)
19	17, 18	eleqtrrd 2872	. . . . . . . . . 10 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ∅ ∈ 𝐵)
20		n0i 4301	. . . . . . . . . 10 ⊢ (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
21	19, 20	syl 18	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ 𝐵 = ∅)
22	21	pm2.21d 122	. . . . . . . 8 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
23	22	adantl 486	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐸))
24	23	impancom 456	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
25		nlim0 6422	. . . . . . . . 9 ⊢ ¬ Lim ∅
26		limeq 6373	. . . . . . . . 9 ⊢ (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
27	25, 26	mtbiri 330	. . . . . . . 8 ⊢ (𝐵 = ∅ → ¬ Lim 𝐵)
28	27	adantl 486	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
29	28	pm2.21d 122	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
30	13, 24, 29	3jca 1144	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
31	30	ex 417	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
32	27	con2i 140	. . . . . . . 8 ⊢ (Lim 𝐵 → ¬ 𝐵 = ∅)
33	32	adantl 486	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ¬ 𝐵 = ∅)
34	33	pm2.21d 122	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
35		limeq 6373	. . . . . . . . . . . 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 7838	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → ¬ Lim suc 𝐶)
39	37, 38	impel 514	. . . . . . . . 9 ⊢ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → ¬ Lim 𝐵)
40	39	adantl 486	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → ¬ Lim 𝐵)
41	40	pm2.21d 122	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐸))
42	41	impancom 456	. . . . . 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 1144	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
46	45	ex 417	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
47	31, 46	jaod 872	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
48		1n0 8472	. . . . . . . . 9 ⊢ 1_o ≠ ∅
49		necom 3017	. . . . . . . . . . 11 ⊢ (1_o ≠ ∅ ↔ ∅ ≠ 1_o)
50		df-1o 8453	. . . . . . . . . . . . 13 ⊢ 1_o = suc ∅
51		uni0 4905	. . . . . . . . . . . . . 14 ⊢ ∪ ∅ = ∅
52		suceq 6430	. . . . . . . . . . . . . 14 ⊢ (∪ ∅ = ∅ → suc ∪ ∅ = suc ∅)
53	51, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ suc ∪ ∅ = suc ∅
54	50, 53	eqtr4i 2795	. . . . . . . . . . . 12 ⊢ 1_o = suc ∪ ∅
55	54	neeq2i 3029	. . . . . . . . . . 11 ⊢ (∅ ≠ 1_o ↔ ∅ ≠ suc ∪ ∅)
56		df-ne 2965	. . . . . . . . . . 11 ⊢ (∅ ≠ suc ∪ ∅ ↔ ¬ ∅ = suc ∪ ∅)
57	49, 55, 56	3bitri 300	. . . . . . . . . 10 ⊢ (1_o ≠ ∅ ↔ ¬ ∅ = suc ∪ ∅)
58		id 23	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → 𝐵 = ∅)
59		unieq 4887	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → ∪ 𝐵 = ∪ ∅)
60		suceq 6430	. . . . . . . . . . . . 13 ⊢ (∪ 𝐵 = ∪ ∅ → suc ∪ 𝐵 = suc ∪ ∅)
61	59, 60	syl 18	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → suc ∪ 𝐵 = suc ∪ ∅)
62	58, 61	eqeq12d 2785	. . . . . . . . . . 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 486	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ 𝐵 = ∅)
68	67	pm2.21d 122	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷))
69		simprl 782	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → 𝐵 = suc 𝐶)
70	69	oveq2d 7427	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = (𝐴 ⊗ suc 𝐶))
71		onov0suclim.suc	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)
72	71	adantrl 728	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ suc 𝐶) = 𝐸)
73	70, 72	eqtrd 2804	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶 ∧ 𝐶 ∈ On)) → (𝐴 ⊗ 𝐵) = 𝐸)
74	73	ex 417	. . . . . 6 ⊢ (𝐴 ∈ On → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
75	74	ad2antrr 738	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸))
76		onuni 7787	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ∪ 𝐵 ∈ On)
77		nlimsucg 7838	. . . . . . . . 9 ⊢ (∪ 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
78	76, 77	syl 18	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc ∪ 𝐵)
79		limeq 6373	. . . . . . . . . 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 515	. . . . . . 7 ⊢ ((𝐵 ∈ On ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
83	82	adantll 726	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ¬ Lim 𝐵)
84	83	pm2.21d 122	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))
85	68, 75, 84	3jca 1144	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc ∪ 𝐵) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
86	85	ex 417	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc ∪ 𝐵 → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹))))
87	47, 86	jaod 872	. 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

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∅c0 4294 ∪ cuni 4876 Ord word 6360 Oncon0 6361 Lim wlim 6362 suc csuc 6363 (class class class)co 7411 1_oc1o 8446

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-tr 5223 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fv 6545 df-ov 7414 df-1o 8453

This theorem is referenced by: oa0suclim 43894 om0suclim 43895 oe0suclim 43896

W3C validator