Theorem axrepprim

Description: ax-rep without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010)

	Ref	Expression
Assertion	axrepprim	⊢ ¬ ∀ 𝑥 ¬ ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axrepnd	⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
2		df-ex	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ↔ ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
3		df-an	⊢ ( ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ↔ ¬ ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) )
4	3	exbii	⊢ ( ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑥 ¬ ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) )
5		exnal	⊢ ( ∃ 𝑥 ¬ ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ↔ ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) )
6	4 5	bitri	⊢ ( ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ↔ ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) )
7	6	bibi2i	⊢ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) )
8		dfbi1	⊢ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) ↔ ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) )
9	7 8	bitri	⊢ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ↔ ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) )
10	9	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) )
11	2 10	imbi12i	⊢ ( ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) ) )
12	11	exbii	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ∃ 𝑥 ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) ) )
13		df-ex	⊢ ( ∃ 𝑥 ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) ) ↔ ¬ ∀ 𝑥 ¬ ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) ) )
14	12 13	bitri	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ¬ ∀ 𝑥 ¬ ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) ) )
15	1 14	mpbi	⊢ ¬ ∀ 𝑥 ¬ ( ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ¬ ( ( ∀ 𝑦 𝑧 ∈ 𝑥 → ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) ) → ¬ ( ¬ ∀ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝜑 ) → ∀ 𝑦 𝑧 ∈ 𝑥 ) ) )