Metamath Proof Explorer

Theorem wfac8prim

Description: The class of well-founded sets W models the Axiom of Choice. Since the previous theorems show that all the ZF axioms hold in W , we may use any statement that ZF proves is equivalent to Choice to prove this. We use ac8prim . Part of Corollary II.2.12 of Kunen2 p. 114. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Hypothesis wfax.1 ⊢ W = ⋃ R1 On
Assertion wfac8prim ⊢ ∀ x ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W w ∈ z ∧ ∀ z ∈ W ∀ w ∈ W z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ W y ∈ z → ¬ y ∈ w → ∃ y ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W ∀ v ∈ W v ∈ z ∧ v ∈ y ↔ v = w

Proof

Step Hyp Ref Expression
1 wfax.1 ⊢ W = ⋃ R1 On
2 trwf ⊢ Tr ⁡ ⋃ R1 On
3 treq ⊢ W = ⋃ R1 On → Tr ⁡ W ↔ Tr ⁡ ⋃ R1 On
4 1 3 ax-mp ⊢ Tr ⁡ W ↔ Tr ⁡ ⋃ R1 On
5 2 4 mpbir ⊢ Tr ⁡ W
6 ac8 ⊢ ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ t ∀ z ∈ x ∃! v v ∈ z ∩ t
7 uniwf ⊢ x ∈ ⋃ R1 On ↔ ⋃ x ∈ ⋃ R1 On
8 inss2 ⊢ t ∩ ⋃ x ⊆ ⋃ x
9 sswf ⊢ ⋃ x ∈ ⋃ R1 On ∧ t ∩ ⋃ x ⊆ ⋃ x → t ∩ ⋃ x ∈ ⋃ R1 On
10 8 9 mpan2 ⊢ ⋃ x ∈ ⋃ R1 On → t ∩ ⋃ x ∈ ⋃ R1 On
11 7 10 sylbi ⊢ x ∈ ⋃ R1 On → t ∩ ⋃ x ∈ ⋃ R1 On
12 1 eleq2i ⊢ x ∈ W ↔ x ∈ ⋃ R1 On
13 1 eleq2i ⊢ t ∩ ⋃ x ∈ W ↔ t ∩ ⋃ x ∈ ⋃ R1 On
14 11 12 13 3imtr4i ⊢ x ∈ W → t ∩ ⋃ x ∈ W
15 inss1 ⊢ z ∩ t ⊆ z
16 elssuni ⊢ z ∈ x → z ⊆ ⋃ x
17 15 16 sstrid ⊢ z ∈ x → z ∩ t ⊆ ⋃ x
18 dfss ⊢ z ∩ t ⊆ ⋃ x ↔ z ∩ t = z ∩ t ∩ ⋃ x
19 17 18 sylib ⊢ z ∈ x → z ∩ t = z ∩ t ∩ ⋃ x
20 inass ⊢ z ∩ t ∩ ⋃ x = z ∩ t ∩ ⋃ x
21 19 20 eqtrdi ⊢ z ∈ x → z ∩ t = z ∩ t ∩ ⋃ x
22 21 eleq2d ⊢ z ∈ x → v ∈ z ∩ t ↔ v ∈ z ∩ t ∩ ⋃ x
23 22 eubidv ⊢ z ∈ x → ∃! v v ∈ z ∩ t ↔ ∃! v v ∈ z ∩ t ∩ ⋃ x
24 23 ralbiia ⊢ ∀ z ∈ x ∃! v v ∈ z ∩ t ↔ ∀ z ∈ x ∃! v v ∈ z ∩ t ∩ ⋃ x
25 ineq2 ⊢ y = t ∩ ⋃ x → z ∩ y = z ∩ t ∩ ⋃ x
26 25 eleq2d ⊢ y = t ∩ ⋃ x → v ∈ z ∩ y ↔ v ∈ z ∩ t ∩ ⋃ x
27 26 eubidv ⊢ y = t ∩ ⋃ x → ∃! v v ∈ z ∩ y ↔ ∃! v v ∈ z ∩ t ∩ ⋃ x
28 27 ralbidv ⊢ y = t ∩ ⋃ x → ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ x ∃! v v ∈ z ∩ t ∩ ⋃ x
29 28 rspcev ⊢ t ∩ ⋃ x ∈ W ∧ ∀ z ∈ x ∃! v v ∈ z ∩ t ∩ ⋃ x → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
30 24 29 sylan2b ⊢ t ∩ ⋃ x ∈ W ∧ ∀ z ∈ x ∃! v v ∈ z ∩ t → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
31 14 30 sylan ⊢ x ∈ W ∧ ∀ z ∈ x ∃! v v ∈ z ∩ t → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
32 31 ex ⊢ x ∈ W → ∀ z ∈ x ∃! v v ∈ z ∩ t → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
33 32 exlimdv ⊢ x ∈ W → ∃ t ∀ z ∈ x ∃! v v ∈ z ∩ t → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
34 6 33 syl5 ⊢ x ∈ W → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
35 34 rgen ⊢ ∀ x ∈ W ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y
36 modelac8prim ⊢ Tr ⁡ W → ∀ x ∈ W ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∈ W ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W w ∈ z ∧ ∀ z ∈ W ∀ w ∈ W z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ W y ∈ z → ¬ y ∈ w → ∃ y ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W ∀ v ∈ W v ∈ z ∧ v ∈ y ↔ v = w
37 35 36 mpbii ⊢ Tr ⁡ W → ∀ x ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W w ∈ z ∧ ∀ z ∈ W ∀ w ∈ W z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ W y ∈ z → ¬ y ∈ w → ∃ y ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W ∀ v ∈ W v ∈ z ∧ v ∈ y ↔ v = w
38 5 37 ax-mp ⊢ ∀ x ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W w ∈ z ∧ ∀ z ∈ W ∀ w ∈ W z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ W y ∈ z → ¬ y ∈ w → ∃ y ∈ W ∀ z ∈ W z ∈ x → ∃ w ∈ W ∀ v ∈ W v ∈ z ∧ v ∈ y ↔ v = w