Theorem omsmolem 3195

Description: Lemma for omsmo 3196.

Assertion

Ref	Expression
omsmolem	⊢ (y ∈ ω → (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → (z ∈ y → (F ‘z) ∈ (F ‘y))))

Distinct variable group(s):   x,y,z,A   x,F,y,z

Proof of Theorem omsmolem

Step	Hyp	Ref	Expression
1		eleq2 1150	. . 3 ⊢ (y = ∅ → (z ∈ y ↔ z ∈ ∅))
2		fveq2 2832	. . . 4 ⊢ (y = ∅ → (F ‘y) = (F ‘∅))
3	2	eleq2d 1156	. . 3 ⊢ (y = ∅ → ((F ‘z) ∈ (F ‘y) ↔ (F ‘z) ∈ (F ‘∅)))
4	1, 3	imbi12d 474	. 2 ⊢ (y = ∅ → ((z ∈ y → (F ‘z) ∈ (F ‘y)) ↔ (z ∈ ∅ → (F ‘z) ∈ (F ‘∅))))
5		eleq2 1150	. . 3 ⊢ (y = w → (z ∈ y ↔ z ∈ w))
6		fveq2 2832	. . . 4 ⊢ (y = w → (F ‘y) = (F ‘w))
7	6	eleq2d 1156	. . 3 ⊢ (y = w → ((F ‘z) ∈ (F ‘y) ↔ (F ‘z) ∈ (F ‘w)))
8	5, 7	imbi12d 474	. 2 ⊢ (y = w → ((z ∈ y → (F ‘z) ∈ (F ‘y)) ↔ (z ∈ w → (F ‘z) ∈ (F ‘w))))
9		eleq2 1150	. . 3 ⊢ (y = suc w → (z ∈ y ↔ z ∈ suc w))
10		fveq2 2832	. . . 4 ⊢ (y = suc w → (F ‘y) = (F ‘suc w))
11	10	eleq2d 1156	. . 3 ⊢ (y = suc w → ((F ‘z) ∈ (F ‘y) ↔ (F ‘z) ∈ (F ‘suc w)))
12	9, 11	imbi12d 474	. 2 ⊢ (y = suc w → ((z ∈ y → (F ‘z) ∈ (F ‘y)) ↔ (z ∈ suc w → (F ‘z) ∈ (F ‘suc w))))
13		noel 1711	. . . 4 ⊢ ¬ z ∈ ∅
14	13	pm2.21i 73	. . 3 ⊢ (z ∈ ∅ → (F ‘z) ∈ (F ‘∅))
15	14	a1i 7	. 2 ⊢ (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → (z ∈ ∅ → (F ‘z) ∈ (F ‘∅)))
16		fveq2 2832	. . . . . . . . . . . . 13 ⊢ (x = w → (F ‘x) = (F ‘w))
17		suceq 2288	. . . . . . . . . . . . . 14 ⊢ (x = w → suc x = suc w)
18	17	fveq2d 2836	. . . . . . . . . . . . 13 ⊢ (x = w → (F ‘suc x) = (F ‘suc w))
19	16, 18	eleq12d 1157	. . . . . . . . . . . 12 ⊢ (x = w → ((F ‘x) ∈ (F ‘suc x) ↔ (F ‘w) ∈ (F ‘suc w)))
20	19	rcla4v 1402	. . . . . . . . . . 11 ⊢ (∀x ∈ ω (F ‘x) ∈ (F ‘suc x) → (w ∈ ω → (F ‘w) ∈ (F ‘suc w)))
21	20	imp 277	. . . . . . . . . 10 ⊢ ((∀x ∈ ω (F ‘x) ∈ (F ‘suc x) ∧ w ∈ ω) → (F ‘w) ∈ (F ‘suc w))
22	21	adantll 309	. . . . . . . . 9 ⊢ ((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) → (F ‘w) ∈ (F ‘suc w))
23		ssel 1502	. . . . . . . . . . . . . 14 ⊢ (A ⊆ On → ((F ‘suc w) ∈ A → (F ‘suc w) ∈ On))
24		ffvrn 2890	. . . . . . . . . . . . . . 15 ⊢ ((F:ω–→A ∧ suc w ∈ ω) → (F ‘suc w) ∈ A)
25		peano2b 2388	. . . . . . . . . . . . . . 15 ⊢ (w ∈ ω ↔ suc w ∈ ω)
26	24, 25	sylan2b 347	. . . . . . . . . . . . . 14 ⊢ ((F:ω–→A ∧ w ∈ ω) → (F ‘suc w) ∈ A)
27	23, 26	syl5 22	. . . . . . . . . . . . 13 ⊢ (A ⊆ On → ((F:ω–→A ∧ w ∈ ω) → (F ‘suc w) ∈ On))
28		ontr1 2258	. . . . . . . . . . . . . . 15 ⊢ ((F ‘suc w) ∈ On → (((F ‘z) ∈ (F ‘w) ∧ (F ‘w) ∈ (F ‘suc w)) → (F ‘z) ∈ (F ‘suc w)))
29	28	exp3a 292	. . . . . . . . . . . . . 14 ⊢ ((F ‘suc w) ∈ On → ((F ‘z) ∈ (F ‘w) → ((F ‘w) ∈ (F ‘suc w) → (F ‘z) ∈ (F ‘suc w))))
30	29	com23 32	. . . . . . . . . . . . 13 ⊢ ((F ‘suc w) ∈ On → ((F ‘w) ∈ (F ‘suc w) → ((F ‘z) ∈ (F ‘w) → (F ‘z) ∈ (F ‘suc w))))
31	27, 30	syl6 23	. . . . . . . . . . . 12 ⊢ (A ⊆ On → ((F:ω–→A ∧ w ∈ ω) → ((F ‘w) ∈ (F ‘suc w) → ((F ‘z) ∈ (F ‘w) → (F ‘z) ∈ (F ‘suc w)))))
32	31	exp3a 292	. . . . . . . . . . 11 ⊢ (A ⊆ On → (F:ω–→A → (w ∈ ω → ((F ‘w) ∈ (F ‘suc w) → ((F ‘z) ∈ (F ‘w) → (F ‘z) ∈ (F ‘suc w))))))
33	32	imp31 280	. . . . . . . . . 10 ⊢ (((A ⊆ On ∧ F:ω–→A) ∧ w ∈ ω) → ((F ‘w) ∈ (F ‘suc w) → ((F ‘z) ∈ (F ‘w) → (F ‘z) ∈ (F ‘suc w))))
34	33	adantlr 310	. . . . . . . . 9 ⊢ ((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) → ((F ‘w) ∈ (F ‘suc w) → ((F ‘z) ∈ (F ‘w) → (F ‘z) ∈ (F ‘suc w))))
35	22, 34	mpd 46	. . . . . . . 8 ⊢ ((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) → ((F ‘z) ∈ (F ‘w) → (F ‘z) ∈ (F ‘suc w)))
36	35	syl3d 26	. . . . . . 7 ⊢ ((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) → ((z ∈ w → (F ‘z) ∈ (F ‘w)) → (z ∈ w → (F ‘z) ∈ (F ‘suc w))))
37	36	imp 277	. . . . . 6 ⊢ (((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) ∧ (z ∈ w → (F ‘z) ∈ (F ‘w))) → (z ∈ w → (F ‘z) ∈ (F ‘suc w)))
38		fveq2 2832	. . . . . . . . . . 11 ⊢ (z = w → (F ‘z) = (F ‘w))
39	38	eleq1d 1155	. . . . . . . . . 10 ⊢ (z = w → ((F ‘z) ∈ (F ‘suc w) ↔ (F ‘w) ∈ (F ‘suc w)))
40	39, 21	syl5bir 184	. . . . . . . . 9 ⊢ (z = w → ((∀x ∈ ω (F ‘x) ∈ (F ‘suc x) ∧ w ∈ ω) → (F ‘z) ∈ (F ‘suc w)))
41	40	com12 13	. . . . . . . 8 ⊢ ((∀x ∈ ω (F ‘x) ∈ (F ‘suc x) ∧ w ∈ ω) → (z = w → (F ‘z) ∈ (F ‘suc w)))
42	41	adantll 309	. . . . . . 7 ⊢ ((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) → (z = w → (F ‘z) ∈ (F ‘suc w)))
43	42	adantr 306	. . . . . 6 ⊢ (((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) ∧ (z ∈ w → (F ‘z) ∈ (F ‘w))) → (z = w → (F ‘z) ∈ (F ‘suc w)))
44	37, 43	jaod 329	. . . . 5 ⊢ (((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) ∧ (z ∈ w → (F ‘z) ∈ (F ‘w))) → ((z ∈ w ∨ z = w) → (F ‘z) ∈ (F ‘suc w)))
45		visset 1350	. . . . . 6 ⊢ z ∈ V
46	45	elsuc 2292	. . . . 5 ⊢ (z ∈ suc w ↔ (z ∈ w ∨ z = w))
47	44, 46	syl5ib 181	. . . 4 ⊢ (((((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) ∧ w ∈ ω) ∧ (z ∈ w → (F ‘z) ∈ (F ‘w))) → (z ∈ suc w → (F ‘z) ∈ (F ‘suc w)))
48	47	exp31 293	. . 3 ⊢ (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → (w ∈ ω → ((z ∈ w → (F ‘z) ∈ (F ‘w)) → (z ∈ suc w → (F ‘z) ∈ (F ‘suc w)))))
49	48	com12 13	. 2 ⊢ (w ∈ ω → (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → ((z ∈ w → (F ‘z) ∈ (F ‘w)) → (z ∈ suc w → (F ‘z) ∈ (F ‘suc w)))))
50	4, 8, 12, 15, 49	finds2 2399	1 ⊢ (y ∈ ω → (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → (z ∈ y → (F ‘z) ∈ (F ‘y))))

Syntax hints:   → wi 2   ∨ wo 195   ∧ wa 196   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201   ⊆ wss 1487  ∅c0 1707  Oncon0 2199  suc csuc 2201  ωcom 2372  –→wf 2418   ‘cfv 2422

This theorem is referenced by:  omsmo 3196

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-v 1349  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-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-om 2373  df-xp 2424  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-f 2434  df-fv 2438

metamath.org