Metamath Proof Explorer

Theorem coflim

Description: A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion coflim ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( ∪ 𝐵 = 𝐴 → ( 𝑥 ∈ ∪ 𝐵 ↔ 𝑥 ∈ 𝐴 ) )
2 1 biimprd ⊢ ( ∪ 𝐵 = 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝐵 ) )
3 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
4 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
5 ssel2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐴 )
6 ordelon ⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
7 4 5 6 syl2an ⊢ ( ( Lim 𝐴 ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ On )
8 7 expr ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ On ) )
9 onelss ⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) )
10 8 9 syl6 ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) ) )
11 10 reximdvai ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
12 3 11 syl5bi ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
13 2 12 syl9r ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 = 𝐴 → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
14 13 ralrimdv ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 = 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
15 uniss ⊢ ( 𝐵 ⊆ 𝐴 → ∪ 𝐵 ⊆ ∪ 𝐴 )
16 15 3ad2ant2 ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ∪ 𝐵 ⊆ ∪ 𝐴 )
17 uniss2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵 )
18 17 3ad2ant3 ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ∪ 𝐴 ⊆ ∪ 𝐵 )
19 16 18 eqssd ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ∪ 𝐵 = ∪ 𝐴 )
20 limuni ⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
21 20 3ad2ant1 ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → 𝐴 = ∪ 𝐴 )
22 19 21 eqtr4d ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ∪ 𝐵 = 𝐴 )
23 22 3expia ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐵 = 𝐴 ) )
24 14 23 impbid ⊢ ( ( Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∪ 𝐵 = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )