Theorem unblem2

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

	Ref	Expression
Hypothesis	unblem.2	⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω )
Assertion	unblem2	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		unblem.2	⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω )
2		fveq2	⊢ ( 𝑧 = ∅ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ∅ ) )
3	2	eleq1d	⊢ ( 𝑧 = ∅ → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ↔ ( 𝐹 ‘ ∅ ) ∈ 𝐴 ) )
4		fveq2	⊢ ( 𝑧 = 𝑢 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑢 ) )
5	4	eleq1d	⊢ ( 𝑧 = 𝑢 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑢 ) ∈ 𝐴 ) )
6		fveq2	⊢ ( 𝑧 = suc 𝑢 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ suc 𝑢 ) )
7	6	eleq1d	⊢ ( 𝑧 = suc 𝑢 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ↔ ( 𝐹 ‘ suc 𝑢 ) ∈ 𝐴 ) )
8		omsson	⊢ ω ⊆ On
9		sstr	⊢ ( ( 𝐴 ⊆ ω ∧ ω ⊆ On ) → 𝐴 ⊆ On )
10	8 9	mpan2	⊢ ( 𝐴 ⊆ ω → 𝐴 ⊆ On )
11		peano1	⊢ ∅ ∈ ω
12		eleq1	⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ 𝑣 ↔ ∅ ∈ 𝑣 ) )
13	12	rexbidv	⊢ ( 𝑤 = ∅ → ( ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ↔ ∃ 𝑣 ∈ 𝐴 ∅ ∈ 𝑣 ) )
14	13	rspcv	⊢ ( ∅ ∈ ω → ( ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃ 𝑣 ∈ 𝐴 ∅ ∈ 𝑣 ) )
15	11 14	ax-mp	⊢ ( ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃ 𝑣 ∈ 𝐴 ∅ ∈ 𝑣 )
16		df-rex	⊢ ( ∃ 𝑣 ∈ 𝐴 ∅ ∈ 𝑣 ↔ ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣 ) )
17	15 16	sylib	⊢ ( ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣 ) )
18		exsimpl	⊢ ( ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣 ) → ∃ 𝑣 𝑣 ∈ 𝐴 )
19	17 18	syl	⊢ ( ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃ 𝑣 𝑣 ∈ 𝐴 )
20		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ 𝐴 )
21	19 20	sylibr	⊢ ( ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → 𝐴 ≠ ∅ )
22		onint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )
23	10 21 22	syl2an	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ∩ 𝐴 ∈ 𝐴 )
24	1	fveq1i	⊢ ( 𝐹 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) ‘ ∅ )
25		fr0g	⊢ ( ∩ 𝐴 ∈ 𝐴 → ( ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) ‘ ∅ ) = ∩ 𝐴 )
26	24 25	eqtr2id	⊢ ( ∩ 𝐴 ∈ 𝐴 → ∩ 𝐴 = ( 𝐹 ‘ ∅ ) )
27	26	eleq1d	⊢ ( ∩ 𝐴 ∈ 𝐴 → ( ∩ 𝐴 ∈ 𝐴 ↔ ( 𝐹 ‘ ∅ ) ∈ 𝐴 ) )
28	27	ibi	⊢ ( ∩ 𝐴 ∈ 𝐴 → ( 𝐹 ‘ ∅ ) ∈ 𝐴 )
29	23 28	syl	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝐹 ‘ ∅ ) ∈ 𝐴 )
30		unblem1	⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝐴 ) → ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 )
31		suceq	⊢ ( 𝑦 = 𝑥 → suc 𝑦 = suc 𝑥 )
32	31	difeq2d	⊢ ( 𝑦 = 𝑥 → ( 𝐴 ∖ suc 𝑦 ) = ( 𝐴 ∖ suc 𝑥 ) )
33	32	inteqd	⊢ ( 𝑦 = 𝑥 → ∩ ( 𝐴 ∖ suc 𝑦 ) = ∩ ( 𝐴 ∖ suc 𝑥 ) )
34		suceq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑢 ) → suc 𝑦 = suc ( 𝐹 ‘ 𝑢 ) )
35	34	difeq2d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑢 ) → ( 𝐴 ∖ suc 𝑦 ) = ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) )
36	35	inteqd	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑢 ) → ∩ ( 𝐴 ∖ suc 𝑦 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) )
37	1 33 36	frsucmpt2	⊢ ( ( 𝑢 ∈ ω ∧ ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 ) → ( 𝐹 ‘ suc 𝑢 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) )
38	37	eqcomd	⊢ ( ( 𝑢 ∈ ω ∧ ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 ) → ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) = ( 𝐹 ‘ suc 𝑢 ) )
39	38	eleq1d	⊢ ( ( 𝑢 ∈ ω ∧ ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 ) → ( ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 ↔ ( 𝐹 ‘ suc 𝑢 ) ∈ 𝐴 ) )
40	39	ex	⊢ ( 𝑢 ∈ ω → ( ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 → ( ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 ↔ ( 𝐹 ‘ suc 𝑢 ) ∈ 𝐴 ) ) )
41	40	ibd	⊢ ( 𝑢 ∈ ω → ( ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑢 ) ) ∈ 𝐴 → ( 𝐹 ‘ suc 𝑢 ) ∈ 𝐴 ) )
42	30 41	syl5	⊢ ( 𝑢 ∈ ω → ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝐴 ) → ( 𝐹 ‘ suc 𝑢 ) ∈ 𝐴 ) )
43	42	expd	⊢ ( 𝑢 ∈ ω → ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( ( 𝐹 ‘ 𝑢 ) ∈ 𝐴 → ( 𝐹 ‘ suc 𝑢 ) ∈ 𝐴 ) ) )
44	3 5 7 29 43	finds2	⊢ ( 𝑧 ∈ ω → ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) )
45	44	com12	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) )