oeeui

Description: The division algorithm for ordinal exponentiation. (This version of oeeu gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu .) (Contributed by Mario Carneiro, 25-May-2015)

	Ref	Expression
Hypotheses	oeeu.1	$⊢ X = ⋃ ⋂ \{x \in On \| B \in (A ↑_{𝑜} x)\}$
	oeeu.2	$⊢ P = (ι w \| \exists y \in On \exists z \in (A ↑_{𝑜} X) (w = ⟨y, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B))$
	oeeu.3	$⊢ Y = 1^{st} (P)$
	oeeu.4	$⊢ Z = 2^{nd} (P)$
Assertion	oeeui	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (((C \in On \land D \in (A ∖ 1_{𝑜}) \land E \in (A ↑_{𝑜} C)) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (C = X \land D = Y \land E = Z))$

Proof

Step	Hyp	Ref	Expression
1		oeeu.1	$⊢ X = ⋃ ⋂ \{x \in On \| B \in (A ↑_{𝑜} x)\}$
2		oeeu.2	$⊢ P = (ι w \| \exists y \in On \exists z \in (A ↑_{𝑜} X) (w = ⟨y, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B))$
3		oeeu.3	$⊢ Y = 1^{st} (P)$
4		oeeu.4	$⊢ Z = 2^{nd} (P)$
5		eldifi	$⊢ A \in (On ∖ 2_{𝑜}) \to A \in On$
6	5	adantr	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to A \in On$
7	6	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A \in On$
8		simprl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to C \in On$
9		oecl	$⊢ (A \in On \land C \in On) \to A ↑_{𝑜} C \in On$
10	7 8 9	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} C \in On$
11		om1	$⊢ A ↑_{𝑜} C \in On \to (A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜} = A ↑_{𝑜} C$
12	10 11	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜} = A ↑_{𝑜} C$
13		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
14		dif1o	$⊢ D \in (A ∖ 1_{𝑜}) \leftrightarrow (D \in A \land D \neq \emptyset)$
15	14	simprbi	$⊢ D \in (A ∖ 1_{𝑜}) \to D \neq \emptyset$
16	15	ad2antll	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to D \neq \emptyset$
17		eldifi	$⊢ D \in (A ∖ 1_{𝑜}) \to D \in A$
18	17	ad2antll	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to D \in A$
19		onelon	$⊢ (A \in On \land D \in A) \to D \in On$
20	7 18 19	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to D \in On$
21		on0eln0	$⊢ D \in On \to (\emptyset \in D \leftrightarrow D \neq \emptyset)$
22	20 21	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (\emptyset \in D \leftrightarrow D \neq \emptyset)$
23	16 22	mpbird	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to \emptyset \in D$
24	23	snssd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to \{\emptyset\} \subseteq D$
25	13 24	eqsstrid	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to 1_{𝑜} \subseteq D$
26		1on	$⊢ 1_{𝑜} \in On$
27	26	a1i	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to 1_{𝑜} \in On$
28		omwordi	$⊢ (1_{𝑜} \in On \land D \in On \land A ↑_{𝑜} C \in On) \to (1_{𝑜} \subseteq D \to (A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜} \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} D)$
29	27 20 10 28	syl3anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (1_{𝑜} \subseteq D \to (A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜} \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} D)$
30	25 29	mpd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜} \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} D$
31	12 30	eqsstrrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} C \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} D$
32		omcl	$⊢ (A ↑_{𝑜} C \in On \land D \in On) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \in On$
33	10 20 32	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \in On$
34		simplrl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to E \in (A ↑_{𝑜} C)$
35		onelon	$⊢ (A ↑_{𝑜} C \in On \land E \in (A ↑_{𝑜} C)) \to E \in On$
36	10 34 35	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to E \in On$
37		oaword1	$⊢ ((A ↑_{𝑜} C) \cdot_{𝑜} D \in On \land E \in On) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E$
38	33 36 37	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E$
39		simplrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B$
40	38 39	sseqtrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq B$
41	31 40	sstrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} C \subseteq B$
42	1	oeeulem	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (X \in On \land A ↑_{𝑜} X \subseteq B \land B \in (A ↑_{𝑜} suc X))$
43	42	simp3d	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to B \in (A ↑_{𝑜} suc X)$
44	43	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to B \in (A ↑_{𝑜} suc X)$
45	42	simp1d	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to X \in On$
46	45	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to X \in On$
47		onsuc	$⊢ X \in On \to suc X \in On$
48	46 47	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to suc X \in On$
49		oecl	$⊢ (A \in On \land suc X \in On) \to A ↑_{𝑜} suc X \in On$
50	7 48 49	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} suc X \in On$
51		ontr2	$⊢ (A ↑_{𝑜} C \in On \land A ↑_{𝑜} suc X \in On) \to ((A ↑_{𝑜} C \subseteq B \land B \in (A ↑_{𝑜} suc X)) \to A ↑_{𝑜} C \in (A ↑_{𝑜} suc X))$
52	10 50 51	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to ((A ↑_{𝑜} C \subseteq B \land B \in (A ↑_{𝑜} suc X)) \to A ↑_{𝑜} C \in (A ↑_{𝑜} suc X))$
53	41 44 52	mp2and	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} C \in (A ↑_{𝑜} suc X)$
54		simplll	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A \in (On ∖ 2_{𝑜})$
55		oeord	$⊢ (C \in On \land suc X \in On \land A \in (On ∖ 2_{𝑜})) \to (C \in suc X \leftrightarrow A ↑_{𝑜} C \in (A ↑_{𝑜} suc X))$
56	8 48 54 55	syl3anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (C \in suc X \leftrightarrow A ↑_{𝑜} C \in (A ↑_{𝑜} suc X))$
57	53 56	mpbird	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to C \in suc X$
58		onsssuc	$⊢ (C \in On \land X \in On) \to (C \subseteq X \leftrightarrow C \in suc X)$
59	8 46 58	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (C \subseteq X \leftrightarrow C \in suc X)$
60	57 59	mpbird	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to C \subseteq X$
61	42	simp2d	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to A ↑_{𝑜} X \subseteq B$
62	61	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} X \subseteq B$
63		eloni	$⊢ A \in On \to Ord A$
64	7 63	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to Ord A$
65		ordsucss	$⊢ Ord A \to (D \in A \to suc D \subseteq A)$
66	64 18 65	sylc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to suc D \subseteq A$
67		onsuc	$⊢ D \in On \to suc D \in On$
68	20 67	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to suc D \in On$
69		dif20el	$⊢ A \in (On ∖ 2_{𝑜}) \to \emptyset \in A$
70	54 69	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to \emptyset \in A$
71		oen0	$⊢ ((A \in On \land C \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} C)$
72	7 8 70 71	syl21anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to \emptyset \in (A ↑_{𝑜} C)$
73		omword	$⊢ ((suc D \in On \land A \in On \land A ↑_{𝑜} C \in On) \land \emptyset \in (A ↑_{𝑜} C)) \to (suc D \subseteq A \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} suc D \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} A)$
74	68 7 10 72 73	syl31anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (suc D \subseteq A \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} suc D \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} A)$
75	66 74	mpbid	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} suc D \subseteq (A ↑_{𝑜} C) \cdot_{𝑜} A$
76		oaord	$⊢ (E \in On \land A ↑_{𝑜} C \in On \land (A ↑_{𝑜} C) \cdot_{𝑜} D \in On) \to (E \in (A ↑_{𝑜} C) \leftrightarrow ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E \in (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} (A ↑_{𝑜} C)))$
77	36 10 33 76	syl3anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (E \in (A ↑_{𝑜} C) \leftrightarrow ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E \in (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} (A ↑_{𝑜} C)))$
78	34 77	mpbid	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E \in (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} (A ↑_{𝑜} C))$
79	39 78	eqeltrrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to B \in (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} (A ↑_{𝑜} C))$
80		odi	$⊢ (A ↑_{𝑜} C \in On \land D \in On \land 1_{𝑜} \in On) \to (A ↑_{𝑜} C) \cdot_{𝑜} (D +_{𝑜} 1_{𝑜}) = ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} ((A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜})$
81	10 20 27 80	syl3anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} (D +_{𝑜} 1_{𝑜}) = ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} ((A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜})$
82		oa1suc	$⊢ D \in On \to D +_{𝑜} 1_{𝑜} = suc D$
83	20 82	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to D +_{𝑜} 1_{𝑜} = suc D$
84	83	oveq2d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} (D +_{𝑜} 1_{𝑜}) = (A ↑_{𝑜} C) \cdot_{𝑜} suc D$
85	12	oveq2d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} ((A ↑_{𝑜} C) \cdot_{𝑜} 1_{𝑜}) = ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} (A ↑_{𝑜} C)$
86	81 84 85	3eqtr3d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (A ↑_{𝑜} C) \cdot_{𝑜} suc D = ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} (A ↑_{𝑜} C)$
87	79 86	eleqtrrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to B \in ((A ↑_{𝑜} C) \cdot_{𝑜} suc D)$
88	75 87	sseldd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to B \in ((A ↑_{𝑜} C) \cdot_{𝑜} A)$
89		oesuc	$⊢ (A \in On \land C \in On) \to A ↑_{𝑜} suc C = (A ↑_{𝑜} C) \cdot_{𝑜} A$
90	7 8 89	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} suc C = (A ↑_{𝑜} C) \cdot_{𝑜} A$
91	88 90	eleqtrrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to B \in (A ↑_{𝑜} suc C)$
92		oecl	$⊢ (A \in On \land X \in On) \to A ↑_{𝑜} X \in On$
93	7 46 92	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} X \in On$
94		onsuc	$⊢ C \in On \to suc C \in On$
95	94	ad2antrl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to suc C \in On$
96		oecl	$⊢ (A \in On \land suc C \in On) \to A ↑_{𝑜} suc C \in On$
97	7 95 96	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} suc C \in On$
98		ontr2	$⊢ (A ↑_{𝑜} X \in On \land A ↑_{𝑜} suc C \in On) \to ((A ↑_{𝑜} X \subseteq B \land B \in (A ↑_{𝑜} suc C)) \to A ↑_{𝑜} X \in (A ↑_{𝑜} suc C))$
99	93 97 98	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to ((A ↑_{𝑜} X \subseteq B \land B \in (A ↑_{𝑜} suc C)) \to A ↑_{𝑜} X \in (A ↑_{𝑜} suc C))$
100	62 91 99	mp2and	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to A ↑_{𝑜} X \in (A ↑_{𝑜} suc C)$
101		oeord	$⊢ (X \in On \land suc C \in On \land A \in (On ∖ 2_{𝑜})) \to (X \in suc C \leftrightarrow A ↑_{𝑜} X \in (A ↑_{𝑜} suc C))$
102	46 95 54 101	syl3anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (X \in suc C \leftrightarrow A ↑_{𝑜} X \in (A ↑_{𝑜} suc C))$
103	100 102	mpbird	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to X \in suc C$
104		onsssuc	$⊢ (X \in On \land C \in On) \to (X \subseteq C \leftrightarrow X \in suc C)$
105	46 8 104	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (X \subseteq C \leftrightarrow X \in suc C)$
106	103 105	mpbird	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to X \subseteq C$
107	60 106	eqssd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to C = X$
108	107 20	jca	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C \in On \land D \in (A ∖ 1_{𝑜}))) \to (C = X \land D \in On)$
109		simprl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to C = X$
110	45	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to X \in On$
111	109 110	eqeltrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to C \in On$
112	6	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A \in On$
113	112 111 9	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} C \in On$
114		simprr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to D \in On$
115	113 114 32	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \in On$
116		simplrl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to E \in (A ↑_{𝑜} C)$
117	113 116 35	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to E \in On$
118	115 117 37	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E$
119		simplrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B$
120	118 119	sseqtrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq B$
121	43	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to B \in (A ↑_{𝑜} suc X)$
122		suceq	$⊢ C = X \to suc C = suc X$
123	122	ad2antrl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to suc C = suc X$
124	123	oveq2d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} suc C = A ↑_{𝑜} suc X$
125	112 111 89	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} suc C = (A ↑_{𝑜} C) \cdot_{𝑜} A$
126	124 125	eqtr3d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} suc X = (A ↑_{𝑜} C) \cdot_{𝑜} A$
127	121 126	eleqtrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to B \in ((A ↑_{𝑜} C) \cdot_{𝑜} A)$
128		omcl	$⊢ (A ↑_{𝑜} C \in On \land A \in On) \to (A ↑_{𝑜} C) \cdot_{𝑜} A \in On$
129	113 112 128	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C) \cdot_{𝑜} A \in On$
130		ontr2	$⊢ ((A ↑_{𝑜} C) \cdot_{𝑜} D \in On \land (A ↑_{𝑜} C) \cdot_{𝑜} A \in On) \to (((A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq B \land B \in ((A ↑_{𝑜} C) \cdot_{𝑜} A)) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \in ((A ↑_{𝑜} C) \cdot_{𝑜} A))$
131	115 129 130	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (((A ↑_{𝑜} C) \cdot_{𝑜} D \subseteq B \land B \in ((A ↑_{𝑜} C) \cdot_{𝑜} A)) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \in ((A ↑_{𝑜} C) \cdot_{𝑜} A))$
132	120 127 131	mp2and	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C) \cdot_{𝑜} D \in ((A ↑_{𝑜} C) \cdot_{𝑜} A)$
133	69	adantr	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to \emptyset \in A$
134	133	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to \emptyset \in A$
135	112 111 134 71	syl21anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to \emptyset \in (A ↑_{𝑜} C)$
136		omord2	$⊢ ((D \in On \land A \in On \land A ↑_{𝑜} C \in On) \land \emptyset \in (A ↑_{𝑜} C)) \to (D \in A \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} D \in ((A ↑_{𝑜} C) \cdot_{𝑜} A))$
137	114 112 113 135 136	syl31anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (D \in A \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} D \in ((A ↑_{𝑜} C) \cdot_{𝑜} A))$
138	132 137	mpbird	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to D \in A$
139	109	oveq2d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} C = A ↑_{𝑜} X$
140	61	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} X \subseteq B$
141	139 140	eqsstrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to A ↑_{𝑜} C \subseteq B$
142		eldifi	$⊢ B \in (On ∖ 1_{𝑜}) \to B \in On$
143	142	adantl	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to B \in On$
144	143	ad2antrr	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to B \in On$
145		ontri1	$⊢ (A ↑_{𝑜} C \in On \land B \in On) \to (A ↑_{𝑜} C \subseteq B \leftrightarrow \neg B \in (A ↑_{𝑜} C))$
146	113 144 145	syl2anc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C \subseteq B \leftrightarrow \neg B \in (A ↑_{𝑜} C))$
147	141 146	mpbid	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to \neg B \in (A ↑_{𝑜} C)$
148		om0	$⊢ A ↑_{𝑜} C \in On \to (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset = \emptyset$
149	113 148	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset = \emptyset$
150	149	oveq1d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to ((A ↑_{𝑜} C) \cdot_{𝑜} \emptyset) +_{𝑜} E = \emptyset +_{𝑜} E$
151		oa0r	$⊢ E \in On \to \emptyset +_{𝑜} E = E$
152	117 151	syl	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to \emptyset +_{𝑜} E = E$
153	150 152	eqtrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to ((A ↑_{𝑜} C) \cdot_{𝑜} \emptyset) +_{𝑜} E = E$
154	153 116	eqeltrd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to ((A ↑_{𝑜} C) \cdot_{𝑜} \emptyset) +_{𝑜} E \in (A ↑_{𝑜} C)$
155		oveq2	$⊢ D = \emptyset \to (A ↑_{𝑜} C) \cdot_{𝑜} D = (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset$
156	155	oveq1d	$⊢ D = \emptyset \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = ((A ↑_{𝑜} C) \cdot_{𝑜} \emptyset) +_{𝑜} E$
157	156	eleq1d	$⊢ D = \emptyset \to (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E \in (A ↑_{𝑜} C) \leftrightarrow ((A ↑_{𝑜} C) \cdot_{𝑜} \emptyset) +_{𝑜} E \in (A ↑_{𝑜} C))$
158	154 157	syl5ibrcom	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (D = \emptyset \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E \in (A ↑_{𝑜} C))$
159	119	eleq1d	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E \in (A ↑_{𝑜} C) \leftrightarrow B \in (A ↑_{𝑜} C))$
160	158 159	sylibd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (D = \emptyset \to B \in (A ↑_{𝑜} C))$
161	160	necon3bd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (\neg B \in (A ↑_{𝑜} C) \to D \neq \emptyset)$
162	147 161	mpd	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to D \neq \emptyset$
163	138 162 14	sylanbrc	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to D \in (A ∖ 1_{𝑜})$
164	111 163	jca	$⊢ (((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \land (C = X \land D \in On)) \to (C \in On \land D \in (A ∖ 1_{𝑜}))$
165	108 164	impbida	$⊢ ((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \to ((C \in On \land D \in (A ∖ 1_{𝑜})) \leftrightarrow (C = X \land D \in On))$
166	165	ex	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to ((E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B) \to ((C \in On \land D \in (A ∖ 1_{𝑜})) \leftrightarrow (C = X \land D \in On)))$
167	166	pm5.32rd	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (((C \in On \land D \in (A ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \leftrightarrow ((C = X \land D \in On) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)))$
168		anass	$⊢ ((C = X \land D \in On) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \leftrightarrow (C = X \land (D \in On \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)))$
169	167 168	bitrdi	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (((C \in On \land D \in (A ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \leftrightarrow (C = X \land (D \in On \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B))))$
170		3anass	$⊢ (D \in On \land E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (D \in On \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B))$
171		oveq2	$⊢ C = X \to A ↑_{𝑜} C = A ↑_{𝑜} X$
172	171	eleq2d	$⊢ C = X \to (E \in (A ↑_{𝑜} C) \leftrightarrow E \in (A ↑_{𝑜} X))$
173	171	oveq1d	$⊢ C = X \to (A ↑_{𝑜} C) \cdot_{𝑜} D = (A ↑_{𝑜} X) \cdot_{𝑜} D$
174	173	oveq1d	$⊢ C = X \to ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E$
175	174	eqeq1d	$⊢ C = X \to (((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B)$
176	172 175	3anbi23d	$⊢ C = X \to ((D \in On \land E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (D \in On \land E \in (A ↑_{𝑜} X) \land ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B))$
177	170 176	bitr3id	$⊢ C = X \to ((D \in On \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \leftrightarrow (D \in On \land E \in (A ↑_{𝑜} X) \land ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B))$
178	6 45 92	syl2anc	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to A ↑_{𝑜} X \in On$
179		oen0	$⊢ ((A \in On \land X \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} X)$
180	6 45 133 179	syl21anc	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to \emptyset \in (A ↑_{𝑜} X)$
181	180	ne0d	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to A ↑_{𝑜} X \neq \emptyset$
182		omeu	$⊢ (A ↑_{𝑜} X \in On \land B \in On \land A ↑_{𝑜} X \neq \emptyset) \to \exists! a \exists d \in On \exists e \in (A ↑_{𝑜} X) (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B)$
183		opeq1	$⊢ y = d \to ⟨y, z⟩ = ⟨d, z⟩$
184	183	eqeq2d	$⊢ y = d \to (w = ⟨y, z⟩ \leftrightarrow w = ⟨d, z⟩)$
185		oveq2	$⊢ y = d \to (A ↑_{𝑜} X) \cdot_{𝑜} y = (A ↑_{𝑜} X) \cdot_{𝑜} d$
186	185	oveq1d	$⊢ y = d \to ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} z$
187	186	eqeq1d	$⊢ y = d \to (((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} z = B)$
188	184 187	anbi12d	$⊢ y = d \to ((w = ⟨y, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B) \leftrightarrow (w = ⟨d, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} z = B))$
189		opeq2	$⊢ z = e \to ⟨d, z⟩ = ⟨d, e⟩$
190	189	eqeq2d	$⊢ z = e \to (w = ⟨d, z⟩ \leftrightarrow w = ⟨d, e⟩)$
191		oveq2	$⊢ z = e \to ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} z = ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e$
192	191	eqeq1d	$⊢ z = e \to (((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} z = B \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B)$
193	190 192	anbi12d	$⊢ z = e \to ((w = ⟨d, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} z = B) \leftrightarrow (w = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B))$
194	188 193	cbvrex2vw	$⊢ \exists y \in On \exists z \in (A ↑_{𝑜} X) (w = ⟨y, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B) \leftrightarrow \exists d \in On \exists e \in (A ↑_{𝑜} X) (w = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B)$
195		eqeq1	$⊢ w = a \to (w = ⟨d, e⟩ \leftrightarrow a = ⟨d, e⟩)$
196	195	anbi1d	$⊢ w = a \to ((w = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B) \leftrightarrow (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B))$
197	196	2rexbidv	$⊢ w = a \to (\exists d \in On \exists e \in (A ↑_{𝑜} X) (w = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B) \leftrightarrow \exists d \in On \exists e \in (A ↑_{𝑜} X) (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B))$
198	194 197	bitrid	$⊢ w = a \to (\exists y \in On \exists z \in (A ↑_{𝑜} X) (w = ⟨y, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B) \leftrightarrow \exists d \in On \exists e \in (A ↑_{𝑜} X) (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B))$
199	198	cbviotavw	$⊢ (ι w \| \exists y \in On \exists z \in (A ↑_{𝑜} X) (w = ⟨y, z⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} y) +_{𝑜} z = B)) = (ι a \| \exists d \in On \exists e \in (A ↑_{𝑜} X) (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B))$
200	2 199	eqtri	$⊢ P = (ι a \| \exists d \in On \exists e \in (A ↑_{𝑜} X) (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B))$
201		oveq2	$⊢ d = D \to (A ↑_{𝑜} X) \cdot_{𝑜} d = (A ↑_{𝑜} X) \cdot_{𝑜} D$
202	201	oveq1d	$⊢ d = D \to ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} e$
203	202	eqeq1d	$⊢ d = D \to (((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} e = B)$
204		oveq2	$⊢ e = E \to ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} e = ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E$
205	204	eqeq1d	$⊢ e = E \to (((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} e = B \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B)$
206	200 3 4 203 205	opiota	$⊢ \exists! a \exists d \in On \exists e \in (A ↑_{𝑜} X) (a = ⟨d, e⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} d) +_{𝑜} e = B) \to ((D \in On \land E \in (A ↑_{𝑜} X) \land ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (D = Y \land E = Z))$
207	182 206	syl	$⊢ (A ↑_{𝑜} X \in On \land B \in On \land A ↑_{𝑜} X \neq \emptyset) \to ((D \in On \land E \in (A ↑_{𝑜} X) \land ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (D = Y \land E = Z))$
208	178 143 181 207	syl3anc	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to ((D \in On \land E \in (A ↑_{𝑜} X) \land ((A ↑_{𝑜} X) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (D = Y \land E = Z))$
209	177 208	sylan9bbr	$⊢ ((A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \land C = X) \to ((D \in On \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \leftrightarrow (D = Y \land E = Z))$
210	209	pm5.32da	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to ((C = X \land (D \in On \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B))) \leftrightarrow (C = X \land (D = Y \land E = Z)))$
211	169 210	bitrd	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (((C \in On \land D \in (A ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B)) \leftrightarrow (C = X \land (D = Y \land E = Z)))$
212		3an4anass	$⊢ ((C \in On \land D \in (A ∖ 1_{𝑜}) \land E \in (A ↑_{𝑜} C)) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow ((C \in On \land D \in (A ∖ 1_{𝑜})) \land (E \in (A ↑_{𝑜} C) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B))$
213		3anass	$⊢ (C = X \land D = Y \land E = Z) \leftrightarrow (C = X \land (D = Y \land E = Z))$
214	211 212 213	3bitr4g	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (((C \in On \land D \in (A ∖ 1_{𝑜}) \land E \in (A ↑_{𝑜} C)) \land ((A ↑_{𝑜} C) \cdot_{𝑜} D) +_{𝑜} E = B) \leftrightarrow (C = X \land D = Y \land E = Z))$

Metamath Proof Explorer

Theorem oeeui

Proof