Theorem dfac5prim

Description: dfac5 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Assertion	dfac5prim	⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5	⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
2		n0	⊢ ( 𝑧 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑧 )
3	2	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 𝑤 ∈ 𝑧 )
4		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 𝑤 ∈ 𝑧 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) )
5	3 4	bitri	⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) )
6		df-ne	⊢ ( 𝑧 ≠ 𝑤 ↔ ¬ 𝑧 = 𝑤 )
7		disj1	⊢ ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) )
8	6 7	imbi12i	⊢ ( ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) )
9	8	2ralbii	⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) )
10		r2al	⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) )
11	9 10	bitri	⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) )
12	5 11	anbi12i	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) )
13		elin	⊢ ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) )
14	13	eubii	⊢ ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) )
15		eu6	⊢ ( ∃! 𝑣 ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) )
16	14 15	bitri	⊢ ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) )
17	16	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) )
18		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )
19	17 18	bitri	⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )
20	19	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )
21	12 20	imbi12i	⊢ ( ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) )
22	21	albii	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) )
23	1 22	bitri	⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) )