Metamath Proof Explorer

Theorem dfac5prim

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

Ref Expression
Assertion dfac5prim ⊢ CHOICE ↔ ∀ x ∀ z z ∈ x → ∃ w w ∈ z ∧ ∀ z ∀ w z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y y ∈ z → ¬ y ∈ w → ∃ y ∀ z z ∈ x → ∃ w ∀ v v ∈ z ∧ v ∈ y ↔ v = w

Proof

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