Theorem omeulem1 7549

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

Assertion

Ref	Expression
omeulem1	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem omeulem1

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2 1055	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ On)
2		sucelon 6909	. . . . . 6 ⊢ (𝐵 ∈ On ↔ suc 𝐵 ∈ On)
3	1, 2	sylib 207	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ∈ On)
4		simp1 1054	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On)
5		on0eln0 5697	. . . . . . 7 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
6	5	biimpar 501	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
7	6	3adant2 1073	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
8		omword2 7541	. . . . 5 ⊢ (((suc 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵))
9	3, 4, 7, 8	syl21anc 1317	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵))
10		sucidg 5720	. . . . 5 ⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
11		ssel 3562	. . . . 5 ⊢ (suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵) → (𝐵 ∈ suc 𝐵 → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
12	10, 11	syl5 33	. . . 4 ⊢ (suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵) → (𝐵 ∈ On → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
13	9, 1, 12	sylc 63	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵))
14		suceq 5707	. . . . . 6 ⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
15	14	oveq2d 6565	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ·𝑜 suc 𝑥) = (𝐴 ·𝑜 suc 𝐵))
16	15	eleq2d 2673	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
17	16	rspcev 3282	. . 3 ⊢ ((𝐵 ∈ On ∧ 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
18	1, 13, 17	syl2anc 691	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
19		suceq 5707	. . . . . 6 ⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
20	19	oveq2d 6565	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝐴 ·𝑜 suc 𝑥) = (𝐴 ·𝑜 suc 𝑧))
21	20	eleq2d 2673	. . . 4 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
22	21	onminex 6899	. . 3 ⊢ (∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) → ∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
23		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
24	23	elon 5649	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On ↔ Ord 𝑥)
25		ordzsl 6937	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑥 ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥))
26	24, 25	bitri 263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥))
27		noel 3878	. . . . . . . . . . . . . . . 16 ⊢ ¬ 𝐵 ∈ ∅
28		oveq2 6557	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 ∅))
29		om0x 7486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ·𝑜 ∅) = ∅
30	28, 29	syl6eq 2660	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = ∅)
31	30	eleq2d 2673	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ ∅))
32	27, 31	mtbiri 316	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
33	32	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
34		simp3 1056	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → 𝑥 = suc 𝑤)
35		simp2 1055	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))
36		raleq 3115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = suc 𝑤 → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
37		vex 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
38	37	sucid 5721	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑤 ∈ suc 𝑤
39		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = 𝑤 → suc 𝑧 = suc 𝑤)
40	39	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑤 → (𝐴 ·𝑜 suc 𝑧) = (𝐴 ·𝑜 suc 𝑤))
41	40	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝑤 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
42	41	notbid 307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑤 → (¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
43	42	rspcv 3278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ suc 𝑤 → (∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
44	38, 43	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤))
45	36, 44	syl6bi 242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = suc 𝑤 → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
46	34, 35, 45	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤))
47		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = suc 𝑤 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 suc 𝑤))
48	47	eleq2d 2673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = suc 𝑤 → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
49	48	notbid 307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = suc 𝑤 → (¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
50	49	biimpar 501	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = suc 𝑤 ∧ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
51	34, 46, 50	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
52	51	3expia 1259	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
53	52	rexlimdvw 3016	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (∃𝑤 ∈ On 𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
54		ralnex 2975	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ¬ ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))
55		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → 𝐴 ∈ On)
56	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → 𝑥 ∈ V)
57		simpl 472	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → Lim 𝑥)
58		omlim 7500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ·𝑜 𝑥) = ∪ 𝑧 ∈ 𝑥 (𝐴 ·𝑜 𝑧))
59	55, 56, 57, 58	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 𝑥) = ∪ 𝑧 ∈ 𝑥 (𝐴 ·𝑜 𝑧))
60	59	eleq2d 2673	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ ∪ 𝑧 ∈ 𝑥 (𝐴 ·𝑜 𝑧)))
61		eliun 4460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ ∪ 𝑧 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ↔ ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 𝑧))
62		limord 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Lim 𝑥 → Ord 𝑥)
63	62	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → Ord 𝑥)
64	63, 24	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ On)
65		simp3 1056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑥)
66		onelon 5665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ On)
67	64, 65, 66	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ On)
68		suceloni 6905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ On → suc 𝑧 ∈ On)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → suc 𝑧 ∈ On)
70		simp2 1055	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝐴 ∈ On)
71		sssucid 5719	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧 ⊆ suc 𝑧
72		omwordi 7538	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ suc 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧)))
73	71, 72	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧))
74	67, 69, 70, 73	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧))
75	74	sseld 3567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → (𝐵 ∈ (𝐴 ·𝑜 𝑧) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
76	75	3expia 1259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (𝑧 ∈ 𝑥 → (𝐵 ∈ (𝐴 ·𝑜 𝑧) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))))
77	76	reximdvai 2998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 𝑧) → ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
78	61, 77	syl5bi 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (𝐵 ∈ ∪ 𝑧 ∈ 𝑥 (𝐴 ·𝑜 𝑧) → ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
79	60, 78	sylbid 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
80	79	con3d 147	. . . . . . . . . . . . . . . . . 18 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (¬ ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
81	54, 80	syl5bi 231	. . . . . . . . . . . . . . . . 17 ⊢ ((Lim 𝑥 ∧ 𝐴 ∈ On) → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
82	81	expimpd 627	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑥 → ((𝐴 ∈ On ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
83	82	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ On ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
84	83	3ad2antl1 1216	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
85	33, 53, 84	3jaod 1384	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ((𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
86	26, 85	syl5bi 231	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 ∈ On → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
87	86	impr 647	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
88		simpl1 1057	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐴 ∈ On)
89		simprr 792	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝑥 ∈ On)
90		omcl 7503	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On)
91	88, 89, 90	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·𝑜 𝑥) ∈ On)
92		simpl2 1058	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐵 ∈ On)
93		ontri1 5674	. . . . . . . . . . . 12 ⊢ (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
94	91, 92, 93	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
95	87, 94	mpbird 246	. . . . . . . . . 10 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·𝑜 𝑥) ⊆ 𝐵)
96		oawordex 7524	. . . . . . . . . . 11 ⊢ (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
97	91, 92, 96	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
98	95, 97	mpbid 221	. . . . . . . . 9 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
99	98	3adantr1 1213	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
100		simp3r 1083	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
101		simp21 1087	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
102		simp11 1084	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐴 ∈ On)
103		simp23 1089	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑥 ∈ On)
104		omsuc 7493	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
105	102, 103, 104	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
106	101, 105	eleqtrd 2690	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐵 ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
107	100, 106	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
108		simp3l 1082	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑦 ∈ On)
109	102, 103, 90	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ On)
110		oaord 7514	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜 𝑥) ∈ On) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
111	108, 102, 109, 110	syl3anc 1318	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
112	107, 111	mpbird 246	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑦 ∈ 𝐴)
113	112, 100	jca 553	. . . . . . . . . 10 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝑦 ∈ 𝐴 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
114	113	3expia 1259	. . . . . . . . 9 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) → (𝑦 ∈ 𝐴 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
115	114	reximdv2 2997	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 → ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
116	99, 115	mpd 15	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
117	116	expcom 450	. . . . . 6 ⊢ ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
118	117	3expia 1259	. . . . 5 ⊢ ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
119	118	com13 86	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (𝑥 ∈ On → ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
120	119	reximdvai 2998	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
121	22, 120	syl5 33	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
122	18, 121	mpd 15	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  ∪ ciun 4455  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642  (class class class)co 6549   +_𝑜 coa 7444   ·_𝑜 comu 7445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-omul 7452

This theorem is referenced by:  omeu  7552