Metamath Proof Explorer

Theorem unblem3

Description: Lemma for unbnn . The value of the function F is less than its value at a successor. (Contributed by NM, 3-Dec-2003)

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

Proof

Step Hyp Ref Expression
1 unblem.2 ⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω )
2 1 unblem2 ⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) )
3 2 imp ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 )
4 omsson ⊢ ω ⊆ On
5 sstr ⊢ ( ( 𝐴 ⊆ ω ∧ ω ⊆ On ) → 𝐴 ⊆ On )
6 4 5 mpan2 ⊢ ( 𝐴 ⊆ ω → 𝐴 ⊆ On )
7 ssel ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑧 ) ∈ On ) )
8 7 anc2li ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 → ( 𝐴 ⊆ On ∧ ( 𝐹 ‘ 𝑧 ) ∈ On ) ) )
9 6 8 syl ⊢ ( 𝐴 ⊆ ω → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 → ( 𝐴 ⊆ On ∧ ( 𝐹 ‘ 𝑧 ) ∈ On ) ) )
10 9 ad2antrr ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ 𝑧 ∈ ω ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 → ( 𝐴 ⊆ On ∧ ( 𝐹 ‘ 𝑧 ) ∈ On ) ) )
11 3 10 mpd ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ 𝑧 ∈ ω ) → ( 𝐴 ⊆ On ∧ ( 𝐹 ‘ 𝑧 ) ∈ On ) )
12 onmindif ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝐹 ‘ 𝑧 ) ∈ On ) → ( 𝐹 ‘ 𝑧 ) ∈ ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) )
13 11 12 syl ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ 𝑧 ) ∈ ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) )
14 unblem1 ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) → ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 )
15 14 ex ⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 → ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 ) )
16 2 15 syld ⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 ) )
17 suceq ⊢ ( 𝑦 = 𝑥 → suc 𝑦 = suc 𝑥 )
18 17 difeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐴 ∖ suc 𝑦 ) = ( 𝐴 ∖ suc 𝑥 ) )
19 18 inteqd ⊢ ( 𝑦 = 𝑥 → ∩ ( 𝐴 ∖ suc 𝑦 ) = ∩ ( 𝐴 ∖ suc 𝑥 ) )
20 suceq ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → suc 𝑦 = suc ( 𝐹 ‘ 𝑧 ) )
21 20 difeq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( 𝐴 ∖ suc 𝑦 ) = ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) )
22 21 inteqd ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ∩ ( 𝐴 ∖ suc 𝑦 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) )
23 1 19 22 frsucmpt2 ⊢ ( ( 𝑧 ∈ ω ∧ ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 ) → ( 𝐹 ‘ suc 𝑧 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) )
24 23 ex ⊢ ( 𝑧 ∈ ω → ( ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 → ( 𝐹 ‘ suc 𝑧 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ) )
25 16 24 sylcom ⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ suc 𝑧 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) ) )
26 25 imp ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ suc 𝑧 ) = ∩ ( 𝐴 ∖ suc ( 𝐹 ‘ 𝑧 ) ) )
27 13 26 eleqtrrd ⊢ ( ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) )
28 27 ex ⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) ) )