omeulem1

Description: Lemma for omeu : existence part. (Contributed by Mario Carneiro, 28-Feb-2013)

		Ref	Expression
	Assertion	omeulem1	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to B \in On$
2		onsucb	$⊢ B \in On \leftrightarrow suc B \in On$
3	1 2	sylib	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to suc B \in On$
4		simp1	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to A \in On$
5		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
6	5	biimpar	$⊢ (A \in On \land A \neq \emptyset) \to \emptyset \in A$
7	6	3adant2	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to \emptyset \in A$
8		omword2	$⊢ ((suc B \in On \land A \in On) \land \emptyset \in A) \to suc B \subseteq A \cdot_{𝑜} suc B$
9	3 4 7 8	syl21anc	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to suc B \subseteq A \cdot_{𝑜} suc B$
10		sucidg	$⊢ B \in On \to B \in suc B$
11		ssel	$⊢ suc B \subseteq A \cdot_{𝑜} suc B \to (B \in suc B \to B \in (A \cdot_{𝑜} suc B))$
12	10 11	syl5	$⊢ suc B \subseteq A \cdot_{𝑜} suc B \to (B \in On \to B \in (A \cdot_{𝑜} suc B))$
13	9 1 12	sylc	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to B \in (A \cdot_{𝑜} suc B)$
14		suceq	$⊢ x = B \to suc x = suc B$
15	14	oveq2d	$⊢ x = B \to A \cdot_{𝑜} suc x = A \cdot_{𝑜} suc B$
16	15	eleq2d	$⊢ x = B \to (B \in (A \cdot_{𝑜} suc x) \leftrightarrow B \in (A \cdot_{𝑜} suc B))$
17	16	rspcev	$⊢ (B \in On \land B \in (A \cdot_{𝑜} suc B)) \to \exists x \in On B \in (A \cdot_{𝑜} suc x)$
18	1 13 17	syl2anc	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to \exists x \in On B \in (A \cdot_{𝑜} suc x)$
19		suceq	$⊢ x = z \to suc x = suc z$
20	19	oveq2d	$⊢ x = z \to A \cdot_{𝑜} suc x = A \cdot_{𝑜} suc z$
21	20	eleq2d	$⊢ x = z \to (B \in (A \cdot_{𝑜} suc x) \leftrightarrow B \in (A \cdot_{𝑜} suc z))$
22	21	onminex	$⊢ \exists x \in On B \in (A \cdot_{𝑜} suc x) \to \exists x \in On (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z))$
23		vex	$⊢ x \in V$
24	23	elon	$⊢ x \in On \leftrightarrow Ord x$
25		ordzsl	$⊢ Ord x \leftrightarrow (x = \emptyset \lor \exists w \in On x = suc w \lor Lim x)$
26	24 25	bitri	$⊢ x \in On \leftrightarrow (x = \emptyset \lor \exists w \in On x = suc w \lor Lim x)$
27		oveq2	$⊢ x = \emptyset \to A \cdot_{𝑜} x = A \cdot_{𝑜} \emptyset$
28		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
29	27 28	sylan9eqr	$⊢ (A \in On \land x = \emptyset) \to A \cdot_{𝑜} x = \emptyset$
30		ne0i	$⊢ B \in (A \cdot_{𝑜} x) \to A \cdot_{𝑜} x \neq \emptyset$
31	30	necon2bi	$⊢ A \cdot_{𝑜} x = \emptyset \to \neg B \in (A \cdot_{𝑜} x)$
32	29 31	syl	$⊢ (A \in On \land x = \emptyset) \to \neg B \in (A \cdot_{𝑜} x)$
33	32	ex	$⊢ A \in On \to (x = \emptyset \to \neg B \in (A \cdot_{𝑜} x))$
34	33	a1d	$⊢ A \in On \to (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \to (x = \emptyset \to \neg B \in (A \cdot_{𝑜} x)))$
35	34	3ad2ant1	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \to (x = \emptyset \to \neg B \in (A \cdot_{𝑜} x)))$
36	35	imp	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (x = \emptyset \to \neg B \in (A \cdot_{𝑜} x))$
37		simp3	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x = suc w) \to x = suc w$
38		simp2	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x = suc w) \to \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)$
39		raleq	$⊢ x = suc w \to (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \leftrightarrow \forall z \in suc w \neg B \in (A \cdot_{𝑜} suc z))$
40		vex	$⊢ w \in V$
41	40	sucid	$⊢ w \in suc w$
42		suceq	$⊢ z = w \to suc z = suc w$
43	42	oveq2d	$⊢ z = w \to A \cdot_{𝑜} suc z = A \cdot_{𝑜} suc w$
44	43	eleq2d	$⊢ z = w \to (B \in (A \cdot_{𝑜} suc z) \leftrightarrow B \in (A \cdot_{𝑜} suc w))$
45	44	notbid	$⊢ z = w \to (\neg B \in (A \cdot_{𝑜} suc z) \leftrightarrow \neg B \in (A \cdot_{𝑜} suc w))$
46	45	rspcv	$⊢ w \in suc w \to (\forall z \in suc w \neg B \in (A \cdot_{𝑜} suc z) \to \neg B \in (A \cdot_{𝑜} suc w))$
47	41 46	ax-mp	$⊢ \forall z \in suc w \neg B \in (A \cdot_{𝑜} suc z) \to \neg B \in (A \cdot_{𝑜} suc w)$
48	39 47	syl6bi	$⊢ x = suc w \to (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \to \neg B \in (A \cdot_{𝑜} suc w))$
49	37 38 48	sylc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x = suc w) \to \neg B \in (A \cdot_{𝑜} suc w)$
50		oveq2	$⊢ x = suc w \to A \cdot_{𝑜} x = A \cdot_{𝑜} suc w$
51	50	eleq2d	$⊢ x = suc w \to (B \in (A \cdot_{𝑜} x) \leftrightarrow B \in (A \cdot_{𝑜} suc w))$
52	51	notbid	$⊢ x = suc w \to (\neg B \in (A \cdot_{𝑜} x) \leftrightarrow \neg B \in (A \cdot_{𝑜} suc w))$
53	52	biimpar	$⊢ (x = suc w \land \neg B \in (A \cdot_{𝑜} suc w)) \to \neg B \in (A \cdot_{𝑜} x)$
54	37 49 53	syl2anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x = suc w) \to \neg B \in (A \cdot_{𝑜} x)$
55	54	3expia	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (x = suc w \to \neg B \in (A \cdot_{𝑜} x))$
56	55	rexlimdvw	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (\exists w \in On x = suc w \to \neg B \in (A \cdot_{𝑜} x))$
57		ralnex	$⊢ \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \leftrightarrow \neg \exists z \in x B \in (A \cdot_{𝑜} suc z)$
58		simpr	$⊢ (Lim x \land A \in On) \to A \in On$
59	23	a1i	$⊢ (Lim x \land A \in On) \to x \in V$
60		simpl	$⊢ (Lim x \land A \in On) \to Lim x$
61		omlim	$⊢ (A \in On \land (x \in V \land Lim x)) \to A \cdot_{𝑜} x = ⋃_{z \in x} (A \cdot_{𝑜} z)$
62	58 59 60 61	syl12anc	$⊢ (Lim x \land A \in On) \to A \cdot_{𝑜} x = ⋃_{z \in x} (A \cdot_{𝑜} z)$
63	62	eleq2d	$⊢ (Lim x \land A \in On) \to (B \in (A \cdot_{𝑜} x) \leftrightarrow B \in ⋃_{z \in x} (A \cdot_{𝑜} z))$
64		eliun	$⊢ B \in ⋃_{z \in x} (A \cdot_{𝑜} z) \leftrightarrow \exists z \in x B \in (A \cdot_{𝑜} z)$
65		limord	$⊢ Lim x \to Ord x$
66	65	3ad2ant1	$⊢ (Lim x \land A \in On \land z \in x) \to Ord x$
67	66 24	sylibr	$⊢ (Lim x \land A \in On \land z \in x) \to x \in On$
68		simp3	$⊢ (Lim x \land A \in On \land z \in x) \to z \in x$
69		onelon	$⊢ (x \in On \land z \in x) \to z \in On$
70	67 68 69	syl2anc	$⊢ (Lim x \land A \in On \land z \in x) \to z \in On$
71		onsuc	$⊢ z \in On \to suc z \in On$
72	70 71	syl	$⊢ (Lim x \land A \in On \land z \in x) \to suc z \in On$
73		simp2	$⊢ (Lim x \land A \in On \land z \in x) \to A \in On$
74		sssucid	$⊢ z \subseteq suc z$
75		omwordi	$⊢ (z \in On \land suc z \in On \land A \in On) \to (z \subseteq suc z \to A \cdot_{𝑜} z \subseteq A \cdot_{𝑜} suc z)$
76	74 75	mpi	$⊢ (z \in On \land suc z \in On \land A \in On) \to A \cdot_{𝑜} z \subseteq A \cdot_{𝑜} suc z$
77	70 72 73 76	syl3anc	$⊢ (Lim x \land A \in On \land z \in x) \to A \cdot_{𝑜} z \subseteq A \cdot_{𝑜} suc z$
78	77	sseld	$⊢ (Lim x \land A \in On \land z \in x) \to (B \in (A \cdot_{𝑜} z) \to B \in (A \cdot_{𝑜} suc z))$
79	78	3expia	$⊢ (Lim x \land A \in On) \to (z \in x \to (B \in (A \cdot_{𝑜} z) \to B \in (A \cdot_{𝑜} suc z)))$
80	79	reximdvai	$⊢ (Lim x \land A \in On) \to (\exists z \in x B \in (A \cdot_{𝑜} z) \to \exists z \in x B \in (A \cdot_{𝑜} suc z))$
81	64 80	biimtrid	$⊢ (Lim x \land A \in On) \to (B \in ⋃_{z \in x} (A \cdot_{𝑜} z) \to \exists z \in x B \in (A \cdot_{𝑜} suc z))$
82	63 81	sylbid	$⊢ (Lim x \land A \in On) \to (B \in (A \cdot_{𝑜} x) \to \exists z \in x B \in (A \cdot_{𝑜} suc z))$
83	82	con3d	$⊢ (Lim x \land A \in On) \to (\neg \exists z \in x B \in (A \cdot_{𝑜} suc z) \to \neg B \in (A \cdot_{𝑜} x))$
84	57 83	biimtrid	$⊢ (Lim x \land A \in On) \to (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \to \neg B \in (A \cdot_{𝑜} x))$
85	84	expimpd	$⊢ Lim x \to ((A \in On \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to \neg B \in (A \cdot_{𝑜} x))$
86	85	com12	$⊢ (A \in On \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (Lim x \to \neg B \in (A \cdot_{𝑜} x))$
87	86	3ad2antl1	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (Lim x \to \neg B \in (A \cdot_{𝑜} x))$
88	36 56 87	3jaod	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to ((x = \emptyset \lor \exists w \in On x = suc w \lor Lim x) \to \neg B \in (A \cdot_{𝑜} x))$
89	26 88	biimtrid	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (x \in On \to \neg B \in (A \cdot_{𝑜} x))$
90	89	impr	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to \neg B \in (A \cdot_{𝑜} x)$
91		simpl1	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to A \in On$
92		simprr	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to x \in On$
93		omcl	$⊢ (A \in On \land x \in On) \to A \cdot_{𝑜} x \in On$
94	91 92 93	syl2anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to A \cdot_{𝑜} x \in On$
95		simpl2	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to B \in On$
96		ontri1	$⊢ (A \cdot_{𝑜} x \in On \land B \in On) \to (A \cdot_{𝑜} x \subseteq B \leftrightarrow \neg B \in (A \cdot_{𝑜} x))$
97	94 95 96	syl2anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to (A \cdot_{𝑜} x \subseteq B \leftrightarrow \neg B \in (A \cdot_{𝑜} x))$
98	90 97	mpbird	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to A \cdot_{𝑜} x \subseteq B$
99		oawordex	$⊢ (A \cdot_{𝑜} x \in On \land B \in On) \to (A \cdot_{𝑜} x \subseteq B \leftrightarrow \exists y \in On (A \cdot_{𝑜} x) +_{𝑜} y = B)$
100	94 95 99	syl2anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to (A \cdot_{𝑜} x \subseteq B \leftrightarrow \exists y \in On (A \cdot_{𝑜} x) +_{𝑜} y = B)$
101	98 100	mpbid	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (\forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to \exists y \in On (A \cdot_{𝑜} x) +_{𝑜} y = B$
102	101	3adantr1	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to \exists y \in On (A \cdot_{𝑜} x) +_{𝑜} y = B$
103		simp3r	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to (A \cdot_{𝑜} x) +_{𝑜} y = B$
104		simp21	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to B \in (A \cdot_{𝑜} suc x)$
105		simp11	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to A \in On$
106		simp23	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to x \in On$
107		omsuc	$⊢ (A \in On \land x \in On) \to A \cdot_{𝑜} suc x = (A \cdot_{𝑜} x) +_{𝑜} A$
108	105 106 107	syl2anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to A \cdot_{𝑜} suc x = (A \cdot_{𝑜} x) +_{𝑜} A$
109	104 108	eleqtrd	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to B \in ((A \cdot_{𝑜} x) +_{𝑜} A)$
110	103 109	eqeltrd	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to (A \cdot_{𝑜} x) +_{𝑜} y \in ((A \cdot_{𝑜} x) +_{𝑜} A)$
111		simp3l	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to y \in On$
112	105 106 93	syl2anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to A \cdot_{𝑜} x \in On$
113		oaord	$⊢ (y \in On \land A \in On \land A \cdot_{𝑜} x \in On) \to (y \in A \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} y \in ((A \cdot_{𝑜} x) +_{𝑜} A))$
114	111 105 112 113	syl3anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to (y \in A \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} y \in ((A \cdot_{𝑜} x) +_{𝑜} A))$
115	110 114	mpbird	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to y \in A$
116	115 103	jca	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \land (y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to (y \in A \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
117	116	3expia	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to ((y \in On \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \to (y \in A \land (A \cdot_{𝑜} x) +_{𝑜} y = B))$
118	117	reximdv2	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to (\exists y \in On (A \cdot_{𝑜} x) +_{𝑜} y = B \to \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B)$
119	102 118	mpd	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On)) \to \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B$
120	119	expcom	$⊢ (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z) \land x \in On) \to ((A \in On \land B \in On \land A \neq \emptyset) \to \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B)$
121	120	3expia	$⊢ (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to (x \in On \to ((A \in On \land B \in On \land A \neq \emptyset) \to \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B))$
122	121	com13	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to (x \in On \to ((B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B))$
123	122	reximdvai	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to (\exists x \in On (B \in (A \cdot_{𝑜} suc x) \land \forall z \in x \neg B \in (A \cdot_{𝑜} suc z)) \to \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B)$
124	22 123	syl5	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to (\exists x \in On B \in (A \cdot_{𝑜} suc x) \to \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B)$
125	18 124	mpd	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B$

Metamath Proof Explorer

Theorem omeulem1

Proof