Metamath Proof Explorer


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 ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣𝐴 𝑤𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹𝑧 ) ∈ 𝐴 ) )