Theorem modelac8prim 45451

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

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 𝑀. This, apparently, is because Kunen's statement of the Axiom of Choice uses defined notions, including ∅ and ∩, 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.)

Assertion

Ref	Expression
modelac8prim	⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))

Distinct variable group:   𝑥,𝑧,𝑦,𝑤,𝑣,𝑀

Proof of Theorem modelac8prim

Step	Hyp	Ref	Expression
1		ralabso 45427	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅)))
2		n0abso 45435	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
3	2	adantlr 722	. . . . . . 7 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
4	3	imbi2d 342	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
5	4	ralbidva 3162	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
6	1, 5	bitrd 281	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
7		simpl 484	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → Tr 𝑀)
8		ralabso 45427	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
9	7, 8	ralabsobidv 45431	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
10	9	anabss3 682	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
11		r19.21v 3166	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
12		impexp 452	. . . . . . . . . 10 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
13		df-ne 2937	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝑤 ↔ ¬ 𝑧 = 𝑤)
14	13	imbi1i 351	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅))
15		disjabso 45434	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))
16	15	imbi2d 342	. . . . . . . . . . . 12 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
17	14, 16	bitrid 285	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
18	17	imbi2d 342	. . . . . . . . . 10 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
19	12, 18	bitr3id 287	. . . . . . . . 9 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
20	19	ralbidv 3164	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
21	11, 20	bitr3id 287	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
22	21	ralbidva 3162	. . . . . 6 ⊢ (Tr 𝑀 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
23	22	adantr 482	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
24	10, 23	bitrd 281	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
25	6, 24	anbi12d 639	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))))
26		simpl 484	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → Tr 𝑀)
27		elin 3901	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑦) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
28	27	eubii 2591	. . . . . . . 8 ⊢ (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
29		trel 5190	. . . . . . . . . . . 12 ⊢ (Tr 𝑀 → ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀) → 𝑣 ∈ 𝑀))
30	29	imp 408	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀)) → 𝑣 ∈ 𝑀)
31	30	anass1rs 662	. . . . . . . . . 10 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑣 ∈ 𝑦) → 𝑣 ∈ 𝑀)
32	31	adantrl 723	. . . . . . . . 9 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)) → 𝑣 ∈ 𝑀)
33	32	reueubd 3363	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
34	28, 33	bitr4id 292	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
35		reu6 3669	. . . . . . 7 ⊢ (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))
36	34, 35	bitrdi 289	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
37	26, 36	ralabsobidv 45431	. . . . 5 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
38	37	an32s 659	. . . 4 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑦 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
39	38	rexbidva 3163	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
40	25, 39	imbi12d 346	. 2 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))
41	40	ralbidva 3162	1 ⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∃!weu 2574   ≠ wne 2936  ∀wral 3055  ∃wrex 3065  ∃!wreu 3344   ∩ cin 3884  ∅c0 4264  Tr wtr 5182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-v 3435  df-dif 3888  df-in 3892  df-ss 3902  df-nul 4265  df-uni 4842  df-tr 5183

This theorem is referenced by:  wfac8prim  45461