This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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