Metamath Proof Explorer

Theorem cflem

Description: A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set A . (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion cflem ⊢ A ∈ V → ∃ x ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w

Proof

Step Hyp Ref Expression
1 ssid ⊢ A ⊆ A
2 ssid ⊢ z ⊆ z
3 sseq2 ⊢ w = z → z ⊆ w ↔ z ⊆ z
4 3 rspcev ⊢ z ∈ A ∧ z ⊆ z → ∃ w ∈ A z ⊆ w
5 2 4 mpan2 ⊢ z ∈ A → ∃ w ∈ A z ⊆ w
6 5 rgen ⊢ ∀ z ∈ A ∃ w ∈ A z ⊆ w
7 sseq1 ⊢ y = A → y ⊆ A ↔ A ⊆ A
8 rexeq ⊢ y = A → ∃ w ∈ y z ⊆ w ↔ ∃ w ∈ A z ⊆ w
9 8 ralbidv ⊢ y = A → ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∀ z ∈ A ∃ w ∈ A z ⊆ w
10 7 9 anbi12d ⊢ y = A → y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ A ⊆ A ∧ ∀ z ∈ A ∃ w ∈ A z ⊆ w
11 10 spcegv ⊢ A ∈ V → A ⊆ A ∧ ∀ z ∈ A ∃ w ∈ A z ⊆ w → ∃ y y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
12 1 6 11 mp2ani ⊢ A ∈ V → ∃ y y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
13 fvex ⊢ card ⁡ y ∈ V
14 13 isseti ⊢ ∃ x x = card ⁡ y
15 19.41v ⊢ ∃ x x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∃ x x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
16 14 15 mpbiran ⊢ ∃ x x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
17 16 exbii ⊢ ∃ y ∃ x x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∃ y y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
18 excom ⊢ ∃ y ∃ x x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∃ x ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
19 17 18 bitr3i ⊢ ∃ y y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∃ x ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
20 12 19 sylib ⊢ A ∈ V → ∃ x ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w