Metamath Proof Explorer

Theorem unblem1

Description: Lemma for unbnn . After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003)

Ref Expression
Assertion unblem1 ( ( ( 𝐵 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ∩ ( 𝐵 ∖ suc 𝐴 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 omsson ⊢ ω ⊆ On
2 sstr ⊢ ( ( 𝐵 ⊆ ω ∧ ω ⊆ On ) → 𝐵 ⊆ On )
3 1 2 mpan2 ⊢ ( 𝐵 ⊆ ω → 𝐵 ⊆ On )
4 3 ssdifssd ⊢ ( 𝐵 ⊆ ω → ( 𝐵 ∖ suc 𝐴 ) ⊆ On )
5 4 ad2antrr ⊢ ( ( ( 𝐵 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 ∖ suc 𝐴 ) ⊆ On )
6 ssel ⊢ ( 𝐵 ⊆ ω → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ ω ) )
7 peano2b ⊢ ( 𝐴 ∈ ω ↔ suc 𝐴 ∈ ω )
8 6 7 imbitrdi ⊢ ( 𝐵 ⊆ ω → ( 𝐴 ∈ 𝐵 → suc 𝐴 ∈ ω ) )
9 eleq1 ⊢ ( 𝑥 = suc 𝐴 → ( 𝑥 ∈ 𝑦 ↔ suc 𝐴 ∈ 𝑦 ) )
10 9 rexbidv ⊢ ( 𝑥 = suc 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 suc 𝐴 ∈ 𝑦 ) )
11 10 rspccva ⊢ ( ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ suc 𝐴 ∈ ω ) → ∃ 𝑦 ∈ 𝐵 suc 𝐴 ∈ 𝑦 )
12 ssel ⊢ ( 𝐵 ⊆ ω → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ω ) )
13 nnord ⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
14 ordn2lp ⊢ ( Ord 𝑦 → ¬ ( 𝑦 ∈ suc 𝐴 ∧ suc 𝐴 ∈ 𝑦 ) )
15 imnan ⊢ ( ( 𝑦 ∈ suc 𝐴 → ¬ suc 𝐴 ∈ 𝑦 ) ↔ ¬ ( 𝑦 ∈ suc 𝐴 ∧ suc 𝐴 ∈ 𝑦 ) )
16 14 15 sylibr ⊢ ( Ord 𝑦 → ( 𝑦 ∈ suc 𝐴 → ¬ suc 𝐴 ∈ 𝑦 ) )
17 16 con2d ⊢ ( Ord 𝑦 → ( suc 𝐴 ∈ 𝑦 → ¬ 𝑦 ∈ suc 𝐴 ) )
18 13 17 syl ⊢ ( 𝑦 ∈ ω → ( suc 𝐴 ∈ 𝑦 → ¬ 𝑦 ∈ suc 𝐴 ) )
19 12 18 syl6 ⊢ ( 𝐵 ⊆ ω → ( 𝑦 ∈ 𝐵 → ( suc 𝐴 ∈ 𝑦 → ¬ 𝑦 ∈ suc 𝐴 ) ) )
20 19 imdistand ⊢ ( 𝐵 ⊆ ω → ( ( 𝑦 ∈ 𝐵 ∧ suc 𝐴 ∈ 𝑦 ) → ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ suc 𝐴 ) ) )
21 eldif ⊢ ( 𝑦 ∈ ( 𝐵 ∖ suc 𝐴 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ suc 𝐴 ) )
22 ne0i ⊢ ( 𝑦 ∈ ( 𝐵 ∖ suc 𝐴 ) → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ )
23 21 22 sylbir ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ suc 𝐴 ) → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ )
24 20 23 syl6 ⊢ ( 𝐵 ⊆ ω → ( ( 𝑦 ∈ 𝐵 ∧ suc 𝐴 ∈ 𝑦 ) → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ ) )
25 24 expd ⊢ ( 𝐵 ⊆ ω → ( 𝑦 ∈ 𝐵 → ( suc 𝐴 ∈ 𝑦 → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ ) ) )
26 25 rexlimdv ⊢ ( 𝐵 ⊆ ω → ( ∃ 𝑦 ∈ 𝐵 suc 𝐴 ∈ 𝑦 → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ ) )
27 11 26 syl5 ⊢ ( 𝐵 ⊆ ω → ( ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ suc 𝐴 ∈ ω ) → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ ) )
28 8 27 sylan2d ⊢ ( 𝐵 ⊆ ω → ( ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ ) )
29 28 impl ⊢ ( ( ( 𝐵 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ )
30 onint ⊢ ( ( ( 𝐵 ∖ suc 𝐴 ) ⊆ On ∧ ( 𝐵 ∖ suc 𝐴 ) ≠ ∅ ) → ∩ ( 𝐵 ∖ suc 𝐴 ) ∈ ( 𝐵 ∖ suc 𝐴 ) )
31 5 29 30 syl2anc ⊢ ( ( ( 𝐵 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ∩ ( 𝐵 ∖ suc 𝐴 ) ∈ ( 𝐵 ∖ suc 𝐴 ) )
32 31 eldifad ⊢ ( ( ( 𝐵 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ∩ ( 𝐵 ∖ suc 𝐴 ) ∈ 𝐵 )