Theorem oawordeulem 3156

Description: Lemma for oawordex 3159.

Hypotheses

Ref	Expression
oawordeulem.1	⊢ A ∈ On
oawordeulem.2	⊢ B ∈ On
oawordeulem.3	⊢ S = {y ∈ On∣B ⊆ (A +o y)}

Assertion

Ref	Expression
oawordeulem	⊢ (A ⊆ B → ∃!x ∈ On (A +o x) = B)

Distinct variable group(s):   x,y,A   x,B,y   x,S

Proof of Theorem oawordeulem

Step	Hyp	Ref	Expression
1		oawordeulem.3	. . . . . . . . . . 11 ⊢ S = {y ∈ On∣B ⊆ (A +o y)}
2		ssrab 1556	. . . . . . . . . . 11 ⊢ {y ∈ On∣B ⊆ (A +o y)} ⊆ On
3	1, 2	eqsstr 1530	. . . . . . . . . 10 ⊢ S ⊆ On
4		oawordeulem.2	. . . . . . . . . . . . 13 ⊢ B ∈ On
5		oawordeulem.1	. . . . . . . . . . . . 13 ⊢ A ∈ On
6		oaword2 3155	. . . . . . . . . . . . 13 ⊢ ((B ∈ On ∧ A ∈ On) → B ⊆ (A +o B))
7	4, 5, 6	mp2an 520	. . . . . . . . . . . 12 ⊢ B ⊆ (A +o B)
8	1	eleq2i 1153	. . . . . . . . . . . . . 14 ⊢ (B ∈ S ↔ B ∈ {y ∈ On∣B ⊆ (A +o y)})
9		opreq2 3007	. . . . . . . . . . . . . . . 16 ⊢ (y = B → (A +o y) = (A +o B))
10	9	sseq2d 1528	. . . . . . . . . . . . . . 15 ⊢ (y = B → (B ⊆ (A +o y) ↔ B ⊆ (A +o B)))
11	10	elrab 1422	. . . . . . . . . . . . . 14 ⊢ (B ∈ {y ∈ On∣B ⊆ (A +o y)} ↔ (B ∈ On ∧ B ⊆ (A +o B)))
12	8, 11	bitr 151	. . . . . . . . . . . . 13 ⊢ (B ∈ S ↔ (B ∈ On ∧ B ⊆ (A +o B)))
13	12, 4	mpbiran 547	. . . . . . . . . . . 12 ⊢ (B ∈ S ↔ B ⊆ (A +o B))
14	7, 13	mpbir 165	. . . . . . . . . . 11 ⊢ B ∈ S
15		n0i 1712	. . . . . . . . . . 11 ⊢ (B ∈ S → ¬ S = ∅)
16	14, 15	ax-mp 6	. . . . . . . . . 10 ⊢ ¬ S = ∅
17		oninton 2267	. . . . . . . . . 10 ⊢ ((S ⊆ On ∧ ¬ S = ∅) → ∩S ∈ On)
18	3, 16, 17	mp2an 520	. . . . . . . . 9 ⊢ ∩S ∈ On
19		onzsl 2367	. . . . . . . . 9 ⊢ (∩S ∈ On ↔ (∩S = ∅ ∨ ∃z ∈ On ∩S = suc z ∨ (∩S ∈ V ∧ Lim ∩S)))
20	18, 19	mpbi 164	. . . . . . . 8 ⊢ (∩S = ∅ ∨ ∃z ∈ On ∩S = suc z ∨ (∩S ∈ V ∧ Lim ∩S))
21		opreq2 3007	. . . . . . . . . . . 12 ⊢ (∩S = ∅ → (A +o ∩S) = (A +o ∅))
22		oa0 3124	. . . . . . . . . . . . 13 ⊢ (A ∈ On → (A +o ∅) = A)
23	5, 22	ax-mp 6	. . . . . . . . . . . 12 ⊢ (A +o ∅) = A
24	21, 23	syl6eq 1140	. . . . . . . . . . 11 ⊢ (∩S = ∅ → (A +o ∩S) = A)
25	24	sseq1d 1527	. . . . . . . . . 10 ⊢ (∩S = ∅ → ((A +o ∩S) ⊆ B ↔ A ⊆ B))
26	25	biimprd 136	. . . . . . . . 9 ⊢ (∩S = ∅ → (A ⊆ B → (A +o ∩S) ⊆ B))
27		opreq2 3007	. . . . . . . . . . . . . 14 ⊢ (∩S = suc z → (A +o ∩S) = (A +o suc z))
28		oasuc 3131	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ On ∧ z ∈ On) → (A +o suc z) = suc (A +o z))
29	5, 28	mpan 518	. . . . . . . . . . . . . 14 ⊢ (z ∈ On → (A +o suc z) = suc (A +o z))
30	27, 29	sylan9eqr 1145	. . . . . . . . . . . . 13 ⊢ ((z ∈ On ∧ ∩S = suc z) → (A +o ∩S) = suc (A +o z))
31		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ z ∈ V
32	31	sucid 2304	. . . . . . . . . . . . . . . 16 ⊢ z ∈ suc z
33		eleq2 1150	. . . . . . . . . . . . . . . 16 ⊢ (∩S = suc z → (z ∈ ∩S ↔ z ∈ suc z))
34	32, 33	mpbiri 169	. . . . . . . . . . . . . . 15 ⊢ (∩S = suc z → z ∈ ∩S)
35	18	onel 2346	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ ∩S → z ∈ On)
36		opreq2 3007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = z → (A +o y) = (A +o z))
37	36	sseq2d 1528	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = z → (B ⊆ (A +o y) ↔ B ⊆ (A +o z)))
38	37	onnminsb 2271	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ On → (z ∈ ∩{y ∈ On∣B ⊆ (A +o y)} → ¬ B ⊆ (A +o z)))
39	1	inteqi 1969	. . . . . . . . . . . . . . . . . . 19 ⊢ ∩S = ∩{y ∈ On∣B ⊆ (A +o y)}
40	39	eleq2i 1153	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ ∩S ↔ z ∈ ∩{y ∈ On∣B ⊆ (A +o y)})
41	38, 40	syl5ib 181	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ On → (z ∈ ∩S → ¬ B ⊆ (A +o z)))
42		oacl 3138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ∈ On ∧ z ∈ On) → (A +o z) ∈ On)
43	5, 42	mpan 518	. . . . . . . . . . . . . . . . . . 19 ⊢ (z ∈ On → (A +o z) ∈ On)
44		ontri1 2232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((B ∈ On ∧ (A +o z) ∈ On) → (B ⊆ (A +o z) ↔ ¬ (A +o z) ∈ B))
45	4, 44	mpan 518	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A +o z) ∈ On → (B ⊆ (A +o z) ↔ ¬ (A +o z) ∈ B))
46	43, 45	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ On → (B ⊆ (A +o z) ↔ ¬ (A +o z) ∈ B))
47	46	bicon2d 404	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ On → ((A +o z) ∈ B ↔ ¬ B ⊆ (A +o z)))
48	41, 47	sylibrd 179	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ On → (z ∈ ∩S → (A +o z) ∈ B))
49	35, 48	mpcom 49	. . . . . . . . . . . . . . 15 ⊢ (z ∈ ∩S → (A +o z) ∈ B)
50	4	onord 2343	. . . . . . . . . . . . . . . 16 ⊢ Ord B
51		ordsucss 2320	. . . . . . . . . . . . . . . 16 ⊢ (Ord B → ((A +o z) ∈ B → suc (A +o z) ⊆ B))
52	50, 51	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ ((A +o z) ∈ B → suc (A +o z) ⊆ B)
53	34, 49, 52	3syl 21	. . . . . . . . . . . . . 14 ⊢ (∩S = suc z → suc (A +o z) ⊆ B)
54	53	adantl 305	. . . . . . . . . . . . 13 ⊢ ((z ∈ On ∧ ∩S = suc z) → suc (A +o z) ⊆ B)
55	30, 54	eqsstrd 1534	. . . . . . . . . . . 12 ⊢ ((z ∈ On ∧ ∩S = suc z) → (A +o ∩S) ⊆ B)
56	55	exp 291	. . . . . . . . . . 11 ⊢ (z ∈ On → (∩S = suc z → (A +o ∩S) ⊆ B))
57	56	r19.23aiv 1284	. . . . . . . . . 10 ⊢ (∃z ∈ On ∩S = suc z → (A +o ∩S) ⊆ B)
58	57	a1d 14	. . . . . . . . 9 ⊢ (∃z ∈ On ∩S = suc z → (A ⊆ B → (A +o ∩S) ⊆ B))
59		iunss 2017	. . . . . . . . . . . 12 ⊢ (∪z ∈ ∩ S(A +o z) ⊆ B ↔ ∀z ∈ ∩ S(A +o z) ⊆ B)
60	4	onelss 2348	. . . . . . . . . . . . 13 ⊢ ((A +o z) ∈ B → (A +o z) ⊆ B)
61	49, 60	syl 12	. . . . . . . . . . . 12 ⊢ (z ∈ ∩S → (A +o z) ⊆ B)
62	59, 61	mprgbir 1250	. . . . . . . . . . 11 ⊢ ∪z ∈ ∩ S(A +o z) ⊆ B
63		oalim 3135	. . . . . . . . . . . . 13 ⊢ ((A ∈ On ∧ (∩S ∈ V ∧ Lim ∩S)) → (A +o ∩S) = ∪z ∈ ∩ S(A +o z))
64	5, 63	mpan 518	. . . . . . . . . . . 12 ⊢ ((∩S ∈ V ∧ Lim ∩S) → (A +o ∩S) = ∪z ∈ ∩ S(A +o z))
65	64	sseq1d 1527	. . . . . . . . . . 11 ⊢ ((∩S ∈ V ∧ Lim ∩S) → ((A +o ∩S) ⊆ B ↔ ∪z ∈ ∩ S(A +o z) ⊆ B))
66	62, 65	mpbiri 169	. . . . . . . . . 10 ⊢ ((∩S ∈ V ∧ Lim ∩S) → (A +o ∩S) ⊆ B)
67	66	a1d 14	. . . . . . . . 9 ⊢ ((∩S ∈ V ∧ Lim ∩S) → (A ⊆ B → (A +o ∩S) ⊆ B))
68	26, 58, 67	3jaoi 633	. . . . . . . 8 ⊢ ((∩S = ∅ ∨ ∃z ∈ On ∩S = suc z ∨ (∩S ∈ V ∧ Lim ∩S)) → (A ⊆ B → (A +o ∩S) ⊆ B))
69	20, 68	ax-mp 6	. . . . . . 7 ⊢ (A ⊆ B → (A +o ∩S) ⊆ B)
70	10	rcla4ev 1403	. . . . . . . . . 10 ⊢ ((B ∈ On ∧ B ⊆ (A +o B)) → ∃y ∈ On B ⊆ (A +o y))
71	4, 7, 70	mp2an 520	. . . . . . . . 9 ⊢ ∃y ∈ On B ⊆ (A +o y)
72		ax-17 925	. . . . . . . . . . 11 ⊢ (z ∈ B → ∀y z ∈ B)
73		ax-17 925	. . . . . . . . . . . 12 ⊢ (z ∈ A → ∀y z ∈ A)
74		ax-17 925	. . . . . . . . . . . 12 ⊢ (z ∈ +o → ∀y z ∈ +o )
75		hbrab1 1310	. . . . . . . . . . . . 13 ⊢ (z ∈ {y ∈ On∣B ⊆ (A +o y)} → ∀y z ∈ {y ∈ On∣B ⊆ (A +o y)})
76	75	hbint 1975	. . . . . . . . . . . 12 ⊢ (z ∈ ∩{y ∈ On∣B ⊆ (A +o y)} → ∀y z ∈ ∩{y ∈ On∣B ⊆ (A +o y)})
77	73, 74, 76	hbopr 3017	. . . . . . . . . . 11 ⊢ (z ∈ (A +o ∩{y ∈ On∣B ⊆ (A +o y)}) → ∀y z ∈ (A +o ∩{y ∈ On∣B ⊆ (A +o y)}))
78	72, 77	hbss 1501	. . . . . . . . . 10 ⊢ (B ⊆ (A +o ∩{y ∈ On∣B ⊆ (A +o y)}) → ∀y B ⊆ (A +o ∩{y ∈ On∣B ⊆ (A +o y)}))
79		opreq2 3007	. . . . . . . . . . 11 ⊢ (y = ∩{y ∈ On∣B ⊆ (A +o y)} → (A +o y) = (A +o ∩{y ∈ On∣B ⊆ (A +o y)}))
80	79	sseq2d 1528	. . . . . . . . . 10 ⊢ (y = ∩{y ∈ On∣B ⊆ (A +o y)} → (B ⊆ (A +o y) ↔ B ⊆ (A +o ∩{y ∈ On∣B ⊆ (A +o y)})))
81	78, 80	onminsb 2264	. . . . . . . . 9 ⊢ (∃y ∈ On B ⊆ (A +o y) → B ⊆ (A +o ∩{y ∈ On∣B ⊆ (A +o y)}))
82	71, 81	ax-mp 6	. . . . . . . 8 ⊢ B ⊆ (A +o ∩{y ∈ On∣B ⊆ (A +o y)})
83	39	opreq2i 3010	. . . . . . . 8 ⊢ (A +o ∩S) = (A +o ∩{y ∈ On∣B ⊆ (A +o y)})
84	82, 83	sseqtr4 1533	. . . . . . 7 ⊢ B ⊆ (A +o ∩S)
85	69, 84	jctir 241	. . . . . 6 ⊢ (A ⊆ B → ((A +o ∩S) ⊆ B ∧ B ⊆ (A +o ∩S)))
86		eqss 1516	. . . . . 6 ⊢ ((A +o ∩S) = B ↔ ((A +o ∩S) ⊆ B ∧ B ⊆ (A +o ∩S)))
87	85, 86	sylibr 175	. . . . 5 ⊢ (A ⊆ B → (A +o ∩S) = B)
88	87, 18	jctil 240	. . . 4 ⊢ (A ⊆ B → (∩S ∈ On ∧ (A +o ∩S) = B))
89		opreq2 3007	. . . . . 6 ⊢ (x = ∩S → (A +o x) = (A +o ∩S))
90	89	cleq1d 1109	. . . . 5 ⊢ (x = ∩S → ((A +o x) = B ↔ (A +o ∩S) = B))
91	90	rcla4ev 1403	. . . 4 ⊢ ((∩S ∈ On ∧ (A +o ∩S) = B) → ∃x ∈ On (A +o x) = B)
92	88, 91	syl 12	. . 3 ⊢ (A ⊆ B → ∃x ∈ On (A +o x) = B)
93		oacan 3150	. . . . . 6 ⊢ ((A ∈ On ∧ x ∈ On ∧ y ∈ On) → ((A +o x) = (A +o y) ↔ x = y))
94	5, 93	mp3an1 639	. . . . 5 ⊢ ((x ∈ On ∧ y ∈ On) → ((A +o x) = (A +o y) ↔ x = y))
95		cleqtr 1118	. . . . . 6 ⊢ (((A +o x) = B ∧ B = (A +o y)) → (A +o x) = (A +o y))
96		cleqcom 1103	. . . . . 6 ⊢ ((A +o y) = B ↔ B = (A +o y))
97	95, 96	sylan2b 347	. . . . 5 ⊢ (((A +o x) = B ∧ (A +o y) = B) → (A +o x) = (A +o y))
98	94, 97	syl5bi 183	. . . 4 ⊢ ((x ∈ On ∧ y ∈ On) → (((A +o x) = B ∧ (A +o y) = B) → x = y))
99	98	rgen2 1248	. . 3 ⊢ ∀x ∈ On ∀y ∈ On (((A +o x) = B ∧ (A +o y) = B) → x = y)
100	92, 99	jctir 241	. 2 ⊢ (A ⊆ B → (∃x ∈ On (A +o x) = B ∧ ∀x ∈ On ∀y ∈ On (((A +o x) = B ∧ (A +o y) = B) → x = y)))
101		opreq2 3007	. . . 4 ⊢ (x = y → (A +o x) = (A +o y))
102	101	cleq1d 1109	. . 3 ⊢ (x = y → ((A +o x) = B ↔ (A +o y) = B))
103	102	reu4 1340	. 2 ⊢ (∃!x ∈ On (A +o x) = B ↔ (∃x ∈ On (A +o x) = B ∧ ∀x ∈ On ∀y ∈ On (((A +o x) = B ∧ (A +o y) = B) → x = y)))
104	100, 103	sylibr 175	1 ⊢ (A ⊆ B → ∃!x ∈ On (A +o x) = B)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196   ∨ w3o 580   = weq 797   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  ∃!wreu 1203  {crab 1204  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ∩cint 1965  ∪ciun 1994  Ord word 2198  Oncon0 2199  Lim wlim 2200  suc csuc 2201  (class class class)co 3001   +_o coa 3101

This theorem is referenced by:  oawordeu 3157

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-oadd 3106

metamath.org