zfcndpow

Description: Axiom of Power Sets ax-pow , reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	zfcndpow	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		dtru	⊢ ¬ ∀ 𝑦 𝑦 = 𝑧
2		exnal	⊢ ( ∃ 𝑦 ¬ 𝑦 = 𝑧 ↔ ¬ ∀ 𝑦 𝑦 = 𝑧 )
3	1 2	mpbir	⊢ ∃ 𝑦 ¬ 𝑦 = 𝑧
4		nfe1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
5		axpownd	⊢ ( ¬ 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
6	4 5	exlimi	⊢ ( ∃ 𝑦 ¬ 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
7	3 6	ax-mp	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
8		19.9v	⊢ ( ∃ 𝑥 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 )
9		19.3v	⊢ ( ∀ 𝑧 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 )
10	8 9	imbi12i	⊢ ( ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) )
11	10	albii	⊢ ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) )
12	11	imbi1i	⊢ ( ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
13	12	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
14	13	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( ∃ 𝑥 𝑦 ∈ 𝑧 → ∀ 𝑧 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
15	7 14	mpbi	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
16		elequ1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
17		elequ1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
18	16 17	imbi12d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
19	18	cbvalvw	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) )
20	19	imbi1i	⊢ ( ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
21	20	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
22	21	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
23	15 22	mpbir	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

Metamath Proof Explorer

Theorem zfcndpow

Proof