Theorem unblem2 8774

Description: Lemma for unbnn 8777. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)

Hypothesis

Ref	Expression
unblem.2	⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)

Assertion

Ref	Expression
unblem2	⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴))

Distinct variable groups:   𝑤,𝑣,𝑥,𝑧,𝐴   𝑣,𝐹,𝑤,𝑧

Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem unblem2

Dummy variables 𝑢 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6673	. . . 4 ⊢ (𝑧 = ∅ → (𝐹‘𝑧) = (𝐹‘∅))
2	1	eleq1d 2900	. . 3 ⊢ (𝑧 = ∅ → ((𝐹‘𝑧) ∈ 𝐴 ↔ (𝐹‘∅) ∈ 𝐴))
3		fveq2 6673	. . . 4 ⊢ (𝑧 = 𝑢 → (𝐹‘𝑧) = (𝐹‘𝑢))
4	3	eleq1d 2900	. . 3 ⊢ (𝑧 = 𝑢 → ((𝐹‘𝑧) ∈ 𝐴 ↔ (𝐹‘𝑢) ∈ 𝐴))
5		fveq2 6673	. . . 4 ⊢ (𝑧 = suc 𝑢 → (𝐹‘𝑧) = (𝐹‘suc 𝑢))
6	5	eleq1d 2900	. . 3 ⊢ (𝑧 = suc 𝑢 → ((𝐹‘𝑧) ∈ 𝐴 ↔ (𝐹‘suc 𝑢) ∈ 𝐴))
7		omsson 7587	. . . . . 6 ⊢ ω ⊆ On
8		sstr 3978	. . . . . 6 ⊢ ((𝐴 ⊆ ω ∧ ω ⊆ On) → 𝐴 ⊆ On)
9	7, 8	mpan2 689	. . . . 5 ⊢ (𝐴 ⊆ ω → 𝐴 ⊆ On)
10		peano1 7604	. . . . . . . . 9 ⊢ ∅ ∈ ω
11		eleq1 2903	. . . . . . . . . . 11 ⊢ (𝑤 = ∅ → (𝑤 ∈ 𝑣 ↔ ∅ ∈ 𝑣))
12	11	rexbidv 3300	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → (∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ↔ ∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣))
13	12	rspcv 3621	. . . . . . . . 9 ⊢ (∅ ∈ ω → (∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣))
14	10, 13	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣)
15		df-rex 3147	. . . . . . . 8 ⊢ (∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣 ↔ ∃𝑣(𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣))
16	14, 15	sylib 220	. . . . . . 7 ⊢ (∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃𝑣(𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣))
17		exsimpl 1868	. . . . . . 7 ⊢ (∃𝑣(𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣) → ∃𝑣 𝑣 ∈ 𝐴)
18	16, 17	syl 17	. . . . . 6 ⊢ (∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃𝑣 𝑣 ∈ 𝐴)
19		n0 4313	. . . . . 6 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑣 𝑣 ∈ 𝐴)
20	18, 19	sylibr 236	. . . . 5 ⊢ (∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → 𝐴 ≠ ∅)
21		onint 7513	. . . . 5 ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴)
22	9, 20, 21	syl2an 597	. . . 4 ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → ∩ 𝐴 ∈ 𝐴)
23		unblem.2	. . . . . . . 8 ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)
24	23	fveq1i 6674	. . . . . . 7 ⊢ (𝐹‘∅) = ((rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)‘∅)
25		fr0g 8074	. . . . . . 7 ⊢ (∩ 𝐴 ∈ 𝐴 → ((rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)‘∅) = ∩ 𝐴)
26	24, 25	syl5req 2872	. . . . . 6 ⊢ (∩ 𝐴 ∈ 𝐴 → ∩ 𝐴 = (𝐹‘∅))
27	26	eleq1d 2900	. . . . 5 ⊢ (∩ 𝐴 ∈ 𝐴 → (∩ 𝐴 ∈ 𝐴 ↔ (𝐹‘∅) ∈ 𝐴))
28	27	ibi 269	. . . 4 ⊢ (∩ 𝐴 ∈ 𝐴 → (𝐹‘∅) ∈ 𝐴)
29	22, 28	syl 17	. . 3 ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝐹‘∅) ∈ 𝐴)
30		unblem1 8773	. . . . 5 ⊢ (((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ (𝐹‘𝑢) ∈ 𝐴) → ∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴)
31		suceq 6259	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → suc 𝑦 = suc 𝑥)
32	31	difeq2d 4102	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (𝐴 ∖ suc 𝑦) = (𝐴 ∖ suc 𝑥))
33	32	inteqd 4884	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ∩ (𝐴 ∖ suc 𝑦) = ∩ (𝐴 ∖ suc 𝑥))
34		suceq 6259	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹‘𝑢) → suc 𝑦 = suc (𝐹‘𝑢))
35	34	difeq2d 4102	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑢) → (𝐴 ∖ suc 𝑦) = (𝐴 ∖ suc (𝐹‘𝑢)))
36	35	inteqd 4884	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑢) → ∩ (𝐴 ∖ suc 𝑦) = ∩ (𝐴 ∖ suc (𝐹‘𝑢)))
37	23, 33, 36	frsucmpt2 8079	. . . . . . . . 9 ⊢ ((𝑢 ∈ ω ∧ ∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴) → (𝐹‘suc 𝑢) = ∩ (𝐴 ∖ suc (𝐹‘𝑢)))
38	37	eqcomd 2830	. . . . . . . 8 ⊢ ((𝑢 ∈ ω ∧ ∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴) → ∩ (𝐴 ∖ suc (𝐹‘𝑢)) = (𝐹‘suc 𝑢))
39	38	eleq1d 2900	. . . . . . 7 ⊢ ((𝑢 ∈ ω ∧ ∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴) → (∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴 ↔ (𝐹‘suc 𝑢) ∈ 𝐴))
40	39	ex 415	. . . . . 6 ⊢ (𝑢 ∈ ω → (∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴 → (∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴 ↔ (𝐹‘suc 𝑢) ∈ 𝐴)))
41	40	ibd 271	. . . . 5 ⊢ (𝑢 ∈ ω → (∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴 → (𝐹‘suc 𝑢) ∈ 𝐴))
42	30, 41	syl5 34	. . . 4 ⊢ (𝑢 ∈ ω → (((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ (𝐹‘𝑢) ∈ 𝐴) → (𝐹‘suc 𝑢) ∈ 𝐴))
43	42	expd 418	. . 3 ⊢ (𝑢 ∈ ω → ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → ((𝐹‘𝑢) ∈ 𝐴 → (𝐹‘suc 𝑢) ∈ 𝐴)))
44	2, 4, 6, 29, 43	finds2 7613	. 2 ⊢ (𝑧 ∈ ω → ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝐹‘𝑧) ∈ 𝐴))
45	44	com12 32	1 ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  Vcvv 3497   ∖ cdif 3936   ⊆ wss 3939  ∅c0 4294  ∩ cint 4879   ↦ cmpt 5149   ↾ cres 5560  Oncon0 6194  suc csuc 6196  ‘cfv 6358  ωcom 7583  reccrdg 8048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-om 7584  df-wrecs 7950  df-recs 8011  df-rdg 8049

This theorem is referenced by:  unblem3  8775  unblem4  8776