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 → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-pw	⊢ 𝒫 𝑥 = { 𝑣 ∣ 𝑣 ⊆ 𝑥 }
2		vex	⊢ 𝑥 ∈ V
3		eleq2w2	⊢ ( Fin = V → ( 𝑥 ∈ Fin ↔ 𝑥 ∈ V ) )
4		pwfi	⊢ ( 𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Fin )
5	3 4	bitr3di	⊢ ( Fin = V → ( 𝑥 ∈ V ↔ 𝒫 𝑥 ∈ Fin ) )
6	2 5	mpbii	⊢ ( Fin = V → 𝒫 𝑥 ∈ Fin )
7	6	elexd	⊢ ( Fin = V → 𝒫 𝑥 ∈ V )
8	1 7	eqeltrrid	⊢ ( Fin = V → { 𝑣 ∣ 𝑣 ⊆ 𝑥 } ∈ V )
9		elisset	⊢ ( { 𝑣 ∣ 𝑣 ⊆ 𝑥 } ∈ V → ∃ 𝑦 𝑦 = { 𝑣 ∣ 𝑣 ⊆ 𝑥 } )
10	8 9	syl	⊢ ( Fin = V → ∃ 𝑦 𝑦 = { 𝑣 ∣ 𝑣 ⊆ 𝑥 } )
11		sseq1	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥 ) )
12	11	eqabbw	⊢ ( 𝑦 = { 𝑣 ∣ 𝑣 ⊆ 𝑥 } ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) )
13	12	exbii	⊢ ( ∃ 𝑦 𝑦 = { 𝑣 ∣ 𝑣 ⊆ 𝑥 } ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) )
14	10 13	sylib	⊢ ( Fin = V → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) )
15		biimpr	⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) → ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) )
16	15	alimi	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) → ∀ 𝑧 ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) )
17	16	eximi	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) )
18	14 17	syl	⊢ ( Fin = V → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) )
19		df-ss	⊢ ( 𝑧 ⊆ 𝑥 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
20	19	imbi1i	⊢ ( ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
21	20	albii	⊢ ( ∀ 𝑧 ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
22	21	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
23	18 22	sylib	⊢ ( Fin = V → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )