onov0suclim

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

	Ref	Expression
Hypotheses	onov0suclim.0	$⊢ A \in On \to A \underset{˙}{\otimes} \emptyset = D$
	onov0suclim.suc	$⊢ (A \in On \land C \in On) \to A \underset{˙}{\otimes} suc C = E$
	onov0suclim.lim	$⊢ ((A \in On \land B \in On) \land Lim B) \to A \underset{˙}{\otimes} B = F$
Assertion	onov0suclim	$⊢ (A \in On \land B \in On) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F))$

Proof

Step	Hyp	Ref	Expression
1		onov0suclim.0	$⊢ A \in On \to A \underset{˙}{\otimes} \emptyset = D$
2		onov0suclim.suc	$⊢ (A \in On \land C \in On) \to A \underset{˙}{\otimes} suc C = E$
3		onov0suclim.lim	$⊢ ((A \in On \land B \in On) \land Lim B) \to A \underset{˙}{\otimes} B = F$
4		eloni	$⊢ B \in On \to Ord B$
5		orduniorsuc	$⊢ Ord B \to (B = ⋃ B \lor B = suc ⋃ B)$
6		unizlim	$⊢ Ord B \to (B = ⋃ B \leftrightarrow (B = \emptyset \lor Lim B))$
7	6	biimpd	$⊢ Ord B \to (B = ⋃ B \to (B = \emptyset \lor Lim B))$
8	7	orim1d	$⊢ Ord B \to ((B = ⋃ B \lor B = suc ⋃ B) \to ((B = \emptyset \lor Lim B) \lor B = suc ⋃ B))$
9	5 8	mpd	$⊢ Ord B \to ((B = \emptyset \lor Lim B) \lor B = suc ⋃ B)$
10	4 9	syl	$⊢ B \in On \to ((B = \emptyset \lor Lim B) \lor B = suc ⋃ B)$
11	10	adantl	$⊢ (A \in On \land B \in On) \to ((B = \emptyset \lor Lim B) \lor B = suc ⋃ B)$
12		oveq2	$⊢ B = \emptyset \to A \underset{˙}{\otimes} B = A \underset{˙}{\otimes} \emptyset$
13	12 1	sylan9eqr	$⊢ (A \in On \land B = \emptyset) \to A \underset{˙}{\otimes} B = D$
14	13	ex	$⊢ A \in On \to (B = \emptyset \to A \underset{˙}{\otimes} B = D)$
15	14	ad2antrr	$⊢ ((A \in On \land B \in On) \land B = \emptyset) \to (B = \emptyset \to A \underset{˙}{\otimes} B = D)$
16		eloni	$⊢ C \in On \to Ord C$
17		0elsuc	$⊢ Ord C \to \emptyset \in suc C$
18	16 17	syl	$⊢ C \in On \to \emptyset \in suc C$
19	18	adantl	$⊢ (B = suc C \land C \in On) \to \emptyset \in suc C$
20		simpl	$⊢ (B = suc C \land C \in On) \to B = suc C$
21	19 20	eleqtrrd	$⊢ (B = suc C \land C \in On) \to \emptyset \in B$
22		n0i	$⊢ \emptyset \in B \to \neg B = \emptyset$
23	21 22	syl	$⊢ (B = suc C \land C \in On) \to \neg B = \emptyset$
24	23	pm2.21d	$⊢ (B = suc C \land C \in On) \to (B = \emptyset \to A \underset{˙}{\otimes} B = E)$
25	24	adantl	$⊢ ((A \in On \land B \in On) \land (B = suc C \land C \in On)) \to (B = \emptyset \to A \underset{˙}{\otimes} B = E)$
26	25	impancom	$⊢ ((A \in On \land B \in On) \land B = \emptyset) \to ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E)$
27		nlim0	$⊢ \neg Lim \emptyset$
28		limeq	$⊢ B = \emptyset \to (Lim B \leftrightarrow Lim \emptyset)$
29	27 28	mtbiri	$⊢ B = \emptyset \to \neg Lim B$
30	29	adantl	$⊢ ((A \in On \land B \in On) \land B = \emptyset) \to \neg Lim B$
31	30	pm2.21d	$⊢ ((A \in On \land B \in On) \land B = \emptyset) \to (Lim B \to A \underset{˙}{\otimes} B = F)$
32	15 26 31	3jca	$⊢ ((A \in On \land B \in On) \land B = \emptyset) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F))$
33	32	ex	$⊢ (A \in On \land B \in On) \to (B = \emptyset \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F)))$
34	29	con2i	$⊢ Lim B \to \neg B = \emptyset$
35	34	adantl	$⊢ ((A \in On \land B \in On) \land Lim B) \to \neg B = \emptyset$
36	35	pm2.21d	$⊢ ((A \in On \land B \in On) \land Lim B) \to (B = \emptyset \to A \underset{˙}{\otimes} B = D)$
37		limeq	$⊢ B = suc C \to (Lim B \leftrightarrow Lim suc C)$
38	37	notbid	$⊢ B = suc C \to (\neg Lim B \leftrightarrow \neg Lim suc C)$
39	38	biimprd	$⊢ B = suc C \to (\neg Lim suc C \to \neg Lim B)$
40		nlimsucg	$⊢ C \in On \to \neg Lim suc C$
41	39 40	impel	$⊢ (B = suc C \land C \in On) \to \neg Lim B$
42	41	adantl	$⊢ ((A \in On \land B \in On) \land (B = suc C \land C \in On)) \to \neg Lim B$
43	42	pm2.21d	$⊢ ((A \in On \land B \in On) \land (B = suc C \land C \in On)) \to (Lim B \to A \underset{˙}{\otimes} B = E)$
44	43	impancom	$⊢ ((A \in On \land B \in On) \land Lim B) \to ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E)$
45	3	a1d	$⊢ ((A \in On \land B \in On) \land Lim B) \to (Lim B \to A \underset{˙}{\otimes} B = F)$
46	36 44 45	3jca	$⊢ ((A \in On \land B \in On) \land Lim B) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F))$
47	46	ex	$⊢ (A \in On \land B \in On) \to (Lim B \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F)))$
48	33 47	jaod	$⊢ (A \in On \land B \in On) \to ((B = \emptyset \lor Lim B) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F)))$
49		1n0	$⊢ 1_{𝑜} \neq \emptyset$
50		necom	$⊢ 1_{𝑜} \neq \emptyset \leftrightarrow \emptyset \neq 1_{𝑜}$
51		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
52		uni0	$⊢ ⋃ \emptyset = \emptyset$
53		suceq	$⊢ ⋃ \emptyset = \emptyset \to suc ⋃ \emptyset = suc \emptyset$
54	52 53	ax-mp	$⊢ suc ⋃ \emptyset = suc \emptyset$
55	51 54	eqtr4i	$⊢ 1_{𝑜} = suc ⋃ \emptyset$
56	55	neeq2i	$⊢ \emptyset \neq 1_{𝑜} \leftrightarrow \emptyset \neq suc ⋃ \emptyset$
57		df-ne	$⊢ \emptyset \neq suc ⋃ \emptyset \leftrightarrow \neg \emptyset = suc ⋃ \emptyset$
58	50 56 57	3bitri	$⊢ 1_{𝑜} \neq \emptyset \leftrightarrow \neg \emptyset = suc ⋃ \emptyset$
59		id	$⊢ B = \emptyset \to B = \emptyset$
60		unieq	$⊢ B = \emptyset \to ⋃ B = ⋃ \emptyset$
61		suceq	$⊢ ⋃ B = ⋃ \emptyset \to suc ⋃ B = suc ⋃ \emptyset$
62	60 61	syl	$⊢ B = \emptyset \to suc ⋃ B = suc ⋃ \emptyset$
63	59 62	eqeq12d	$⊢ B = \emptyset \to (B = suc ⋃ B \leftrightarrow \emptyset = suc ⋃ \emptyset)$
64	63	notbid	$⊢ B = \emptyset \to (\neg B = suc ⋃ B \leftrightarrow \neg \emptyset = suc ⋃ \emptyset)$
65	58 64	bitr4id	$⊢ B = \emptyset \to (1_{𝑜} \neq \emptyset \leftrightarrow \neg B = suc ⋃ B)$
66	49 65	mpbii	$⊢ B = \emptyset \to \neg B = suc ⋃ B$
67	66	con2i	$⊢ B = suc ⋃ B \to \neg B = \emptyset$
68	67	adantl	$⊢ ((A \in On \land B \in On) \land B = suc ⋃ B) \to \neg B = \emptyset$
69	68	pm2.21d	$⊢ ((A \in On \land B \in On) \land B = suc ⋃ B) \to (B = \emptyset \to A \underset{˙}{\otimes} B = D)$
70		simprl	$⊢ (A \in On \land (B = suc C \land C \in On)) \to B = suc C$
71	70	oveq2d	$⊢ (A \in On \land (B = suc C \land C \in On)) \to A \underset{˙}{\otimes} B = A \underset{˙}{\otimes} suc C$
72	2	adantrl	$⊢ (A \in On \land (B = suc C \land C \in On)) \to A \underset{˙}{\otimes} suc C = E$
73	71 72	eqtrd	$⊢ (A \in On \land (B = suc C \land C \in On)) \to A \underset{˙}{\otimes} B = E$
74	73	ex	$⊢ A \in On \to ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E)$
75	74	ad2antrr	$⊢ ((A \in On \land B \in On) \land B = suc ⋃ B) \to ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E)$
76		onuni	$⊢ B \in On \to ⋃ B \in On$
77		nlimsucg	$⊢ ⋃ B \in On \to \neg Lim suc ⋃ B$
78	76 77	syl	$⊢ B \in On \to \neg Lim suc ⋃ B$
79		limeq	$⊢ B = suc ⋃ B \to (Lim B \leftrightarrow Lim suc ⋃ B)$
80	79	notbid	$⊢ B = suc ⋃ B \to (\neg Lim B \leftrightarrow \neg Lim suc ⋃ B)$
81	80	biimprd	$⊢ B = suc ⋃ B \to (\neg Lim suc ⋃ B \to \neg Lim B)$
82	78 81	mpan9	$⊢ (B \in On \land B = suc ⋃ B) \to \neg Lim B$
83	82	adantll	$⊢ ((A \in On \land B \in On) \land B = suc ⋃ B) \to \neg Lim B$
84	83	pm2.21d	$⊢ ((A \in On \land B \in On) \land B = suc ⋃ B) \to (Lim B \to A \underset{˙}{\otimes} B = F)$
85	69 75 84	3jca	$⊢ ((A \in On \land B \in On) \land B = suc ⋃ B) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F))$
86	85	ex	$⊢ (A \in On \land B \in On) \to (B = suc ⋃ B \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F)))$
87	48 86	jaod	$⊢ (A \in On \land B \in On) \to (((B = \emptyset \lor Lim B) \lor B = suc ⋃ B) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F)))$
88	11 87	mpd	$⊢ (A \in On \land B \in On) \to ((B = \emptyset \to A \underset{˙}{\otimes} B = D) \land ((B = suc C \land C \in On) \to A \underset{˙}{\otimes} B = E) \land (Lim B \to A \underset{˙}{\otimes} B = F))$

Metamath Proof Explorer

Theorem onov0suclim

Proof