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 ⁡ A ∧ B ⊆ A → ⋃ B = A ↔ ∀ x ∈ A ∃ y ∈ B x ⊆ y

Proof

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