Metamath Proof Explorer

Theorem cfslbn

Description: Any subset of A smaller than its cofinality has union less than A . (This is the contrapositive to cfslb .) (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis cfslb.1 ⊢ 𝐴 ∈ V
Assertion cfslbn ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≺ ( cf ‘ 𝐴 ) ) → ∪ 𝐵 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 cfslb.1 ⊢ 𝐴 ∈ V
2 uniss ⊢ ( 𝐵 ⊆ 𝐴 → ∪ 𝐵 ⊆ ∪ 𝐴 )
3 limuni ⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
4 3 sseq2d ⊢ ( Lim 𝐴 → ( ∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ ∪ 𝐴 ) )
5 2 4 imbitrrid ⊢ ( Lim 𝐴 → ( 𝐵 ⊆ 𝐴 → ∪ 𝐵 ⊆ 𝐴 ) )
6 5 imp ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ∪ 𝐵 ⊆ 𝐴 )
7 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
8 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
9 7 8 syl ⊢ ( Lim 𝐴 → 𝐴 ⊆ On )
10 sstr2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ⊆ On → 𝐵 ⊆ On ) )
11 9 10 syl5com ⊢ ( Lim 𝐴 → ( 𝐵 ⊆ 𝐴 → 𝐵 ⊆ On ) )
12 ssorduni ⊢ ( 𝐵 ⊆ On → Ord ∪ 𝐵 )
13 11 12 syl6 ⊢ ( Lim 𝐴 → ( 𝐵 ⊆ 𝐴 → Ord ∪ 𝐵 ) )
14 13 7 jctird ⊢ ( Lim 𝐴 → ( 𝐵 ⊆ 𝐴 → ( Ord ∪ 𝐵 ∧ Ord 𝐴 ) ) )
15 ordsseleq ⊢ ( ( Ord ∪ 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ ( ∪ 𝐵 ∈ 𝐴 ∨ ∪ 𝐵 = 𝐴 ) ) )
16 14 15 syl6 ⊢ ( Lim 𝐴 → ( 𝐵 ⊆ 𝐴 → ( ∪ 𝐵 ⊆ 𝐴 ↔ ( ∪ 𝐵 ∈ 𝐴 ∨ ∪ 𝐵 = 𝐴 ) ) ) )
17 16 imp ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ ( ∪ 𝐵 ∈ 𝐴 ∨ ∪ 𝐵 = 𝐴 ) ) )
18 6 17 mpbid ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 ∈ 𝐴 ∨ ∪ 𝐵 = 𝐴 ) )
19 18 ord ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ¬ ∪ 𝐵 ∈ 𝐴 → ∪ 𝐵 = 𝐴 ) )
20 1 cfslb ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴 ) → ( cf ‘ 𝐴 ) ≼ 𝐵 )
21 domnsym ⊢ ( ( cf ‘ 𝐴 ) ≼ 𝐵 → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) )
22 20 21 syl ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴 ) → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) )
23 22 3expia ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 = 𝐴 → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) ) )
24 19 23 syld ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ¬ ∪ 𝐵 ∈ 𝐴 → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) ) )
25 24 con4d ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ∪ 𝐵 ∈ 𝐴 ) )
26 25 3impia ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≺ ( cf ‘ 𝐴 ) ) → ∪ 𝐵 ∈ 𝐴 )