Metamath Proof Explorer

Theorem fineqvpow

Description: If all sets are finite, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024)

Ref Expression
Assertion fineqvpow ⊢ Fin = V → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 df-pw ⊢ 𝒫 x = v | v ⊆ x
2 vex ⊢ x ∈ V
3 eleq2w2 ⊢ Fin = V → x ∈ Fin ↔ x ∈ V
4 pwfi ⊢ x ∈ Fin ↔ 𝒫 x ∈ Fin
5 3 4 bitr3di ⊢ Fin = V → x ∈ V ↔ 𝒫 x ∈ Fin
6 2 5 mpbii ⊢ Fin = V → 𝒫 x ∈ Fin
7 6 elexd ⊢ Fin = V → 𝒫 x ∈ V
8 1 7 eqeltrrid ⊢ Fin = V → v | v ⊆ x ∈ V
9 elisset ⊢ v | v ⊆ x ∈ V → ∃ y y = v | v ⊆ x
10 8 9 syl ⊢ Fin = V → ∃ y y = v | v ⊆ x
11 sseq1 ⊢ v = z → v ⊆ x ↔ z ⊆ x
12 11 eqabbw ⊢ y = v | v ⊆ x ↔ ∀ z z ∈ y ↔ z ⊆ x
13 12 exbii ⊢ ∃ y y = v | v ⊆ x ↔ ∃ y ∀ z z ∈ y ↔ z ⊆ x
14 10 13 sylib ⊢ Fin = V → ∃ y ∀ z z ∈ y ↔ z ⊆ x
15 biimpr ⊢ z ∈ y ↔ z ⊆ x → z ⊆ x → z ∈ y
16 15 alimi ⊢ ∀ z z ∈ y ↔ z ⊆ x → ∀ z z ⊆ x → z ∈ y
17 16 eximi ⊢ ∃ y ∀ z z ∈ y ↔ z ⊆ x → ∃ y ∀ z z ⊆ x → z ∈ y
18 14 17 syl ⊢ Fin = V → ∃ y ∀ z z ⊆ x → z ∈ y
19 df-ss ⊢ z ⊆ x ↔ ∀ w w ∈ z → w ∈ x
20 19 imbi1i ⊢ z ⊆ x → z ∈ y ↔ ∀ w w ∈ z → w ∈ x → z ∈ y
21 20 albii ⊢ ∀ z z ⊆ x → z ∈ y ↔ ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
22 21 exbii ⊢ ∃ y ∀ z z ⊆ x → z ∈ y ↔ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
23 18 22 sylib ⊢ Fin = V → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y