Metamath Proof Explorer

Theorem modelac8prim

Description: If M is a transitive class, then the following are equivalent. (1) Every nonempty set x e. M of pairwise disjoint nonempty sets has a choice set in M . (2) The class M models the Axiom of Choice, in the form ac8prim .

Lemma II.2.11(7) of Kunen2 p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in M . This, apparently, is because Kunen's statement of the Axiom of Choice uses defined notions, including (/) and i^i , and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion modelac8prim ⊢ Tr ⁡ M → ∀ x ∈ M ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∈ M ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∈ M ∀ z ∈ M z ∈ x → ∃ w ∈ M w ∈ z ∧ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w → ∃ y ∈ M ∀ z ∈ M z ∈ x → ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w

Proof

Step Hyp Ref Expression
1 ralabso ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ x z ≠ ∅ ↔ ∀ z ∈ M z ∈ x → z ≠ ∅
2 n0abso ⊢ Tr ⁡ M ∧ z ∈ M → z ≠ ∅ ↔ ∃ w ∈ M w ∈ z
3 2 adantlr ⊢ Tr ⁡ M ∧ x ∈ M ∧ z ∈ M → z ≠ ∅ ↔ ∃ w ∈ M w ∈ z
4 3 imbi2d ⊢ Tr ⁡ M ∧ x ∈ M ∧ z ∈ M → z ∈ x → z ≠ ∅ ↔ z ∈ x → ∃ w ∈ M w ∈ z
5 4 ralbidva ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ M z ∈ x → z ≠ ∅ ↔ ∀ z ∈ M z ∈ x → ∃ w ∈ M w ∈ z
6 1 5 bitrd ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ x z ≠ ∅ ↔ ∀ z ∈ M z ∈ x → ∃ w ∈ M w ∈ z
7 simpl ⊢ Tr ⁡ M ∧ x ∈ M → Tr ⁡ M
8 ralabso ⊢ Tr ⁡ M ∧ x ∈ M → ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅
9 7 8 ralabsobidv ⊢ Tr ⁡ M ∧ x ∈ M ∧ x ∈ M → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ M z ∈ x → ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅
10 9 anabss3 ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ M z ∈ x → ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅
11 r19.21v ⊢ ∀ w ∈ M z ∈ x → w ∈ x → z ≠ w → z ∩ w = ∅ ↔ z ∈ x → ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅
12 impexp ⊢ z ∈ x ∧ w ∈ x → z ≠ w → z ∩ w = ∅ ↔ z ∈ x → w ∈ x → z ≠ w → z ∩ w = ∅
13 df-ne ⊢ z ≠ w ↔ ¬ z = w
14 13 imbi1i ⊢ z ≠ w → z ∩ w = ∅ ↔ ¬ z = w → z ∩ w = ∅
15 disjabso ⊢ Tr ⁡ M ∧ z ∈ M → z ∩ w = ∅ ↔ ∀ y ∈ M y ∈ z → ¬ y ∈ w
16 15 imbi2d ⊢ Tr ⁡ M ∧ z ∈ M → ¬ z = w → z ∩ w = ∅ ↔ ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
17 14 16 bitrid ⊢ Tr ⁡ M ∧ z ∈ M → z ≠ w → z ∩ w = ∅ ↔ ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
18 17 imbi2d ⊢ Tr ⁡ M ∧ z ∈ M → z ∈ x ∧ w ∈ x → z ≠ w → z ∩ w = ∅ ↔ z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
19 12 18 bitr3id ⊢ Tr ⁡ M ∧ z ∈ M → z ∈ x → w ∈ x → z ≠ w → z ∩ w = ∅ ↔ z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
20 19 ralbidv ⊢ Tr ⁡ M ∧ z ∈ M → ∀ w ∈ M z ∈ x → w ∈ x → z ≠ w → z ∩ w = ∅ ↔ ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
21 11 20 bitr3id ⊢ Tr ⁡ M ∧ z ∈ M → z ∈ x → ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅ ↔ ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
22 21 ralbidva ⊢ Tr ⁡ M → ∀ z ∈ M z ∈ x → ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
23 22 adantr ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ M z ∈ x → ∀ w ∈ M w ∈ x → z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
24 10 23 bitrd ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
25 6 24 anbi12d ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ M z ∈ x → ∃ w ∈ M w ∈ z ∧ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w
26 simpl ⊢ Tr ⁡ M ∧ y ∈ M → Tr ⁡ M
27 elin ⊢ v ∈ z ∩ y ↔ v ∈ z ∧ v ∈ y
28 27 eubii ⊢ ∃! v v ∈ z ∩ y ↔ ∃! v v ∈ z ∧ v ∈ y
29 trel ⊢ Tr ⁡ M → v ∈ y ∧ y ∈ M → v ∈ M
30 29 imp ⊢ Tr ⁡ M ∧ v ∈ y ∧ y ∈ M → v ∈ M
31 30 anass1rs ⊢ Tr ⁡ M ∧ y ∈ M ∧ v ∈ y → v ∈ M
32 31 adantrl ⊢ Tr ⁡ M ∧ y ∈ M ∧ v ∈ z ∧ v ∈ y → v ∈ M
33 32 reueubd ⊢ Tr ⁡ M ∧ y ∈ M → ∃! v ∈ M v ∈ z ∧ v ∈ y ↔ ∃! v v ∈ z ∧ v ∈ y
34 28 33 bitr4id ⊢ Tr ⁡ M ∧ y ∈ M → ∃! v v ∈ z ∩ y ↔ ∃! v ∈ M v ∈ z ∧ v ∈ y
35 reu6 ⊢ ∃! v ∈ M v ∈ z ∧ v ∈ y ↔ ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w
36 34 35 bitrdi ⊢ Tr ⁡ M ∧ y ∈ M → ∃! v v ∈ z ∩ y ↔ ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w
37 26 36 ralabsobidv ⊢ Tr ⁡ M ∧ y ∈ M ∧ x ∈ M → ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ M z ∈ x → ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w
38 37 an32s ⊢ Tr ⁡ M ∧ x ∈ M ∧ y ∈ M → ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ M z ∈ x → ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w
39 38 rexbidva ⊢ Tr ⁡ M ∧ x ∈ M → ∃ y ∈ M ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∃ y ∈ M ∀ z ∈ M z ∈ x → ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w
40 25 39 imbi12d ⊢ Tr ⁡ M ∧ x ∈ M → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∈ M ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ M z ∈ x → ∃ w ∈ M w ∈ z ∧ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w → ∃ y ∈ M ∀ z ∈ M z ∈ x → ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w
41 40 ralbidva ⊢ Tr ⁡ M → ∀ x ∈ M ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∈ M ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∈ M ∀ z ∈ M z ∈ x → ∃ w ∈ M w ∈ z ∧ ∀ z ∈ M ∀ w ∈ M z ∈ x ∧ w ∈ x → ¬ z = w → ∀ y ∈ M y ∈ z → ¬ y ∈ w → ∃ y ∈ M ∀ z ∈ M z ∈ x → ∃ w ∈ M ∀ v ∈ M v ∈ z ∧ v ∈ y ↔ v = w