Metamath Proof Explorer

Theorem cflemOLD

Description: Obsolete version of cflem as of 25-Jul-2025. (Contributed by NM, 24-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cflemOLD ⊢ 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