Theorem modelac8prim 45419

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 45418.

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 45395	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅)))
2		n0abso 45403	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
3	2	adantlr 716	. . . . . . 7 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
4	3	imbi2d 340	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
5	4	ralbidva 3158	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
6	1, 5	bitrd 279	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
7		simpl 482	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → Tr 𝑀)
8		ralabso 45395	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
9	7, 8	ralabsobidv 45399	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
10	9	anabss3 676	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
11		r19.21v 3162	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
12		impexp 450	. . . . . . . . . 10 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
13		df-ne 2933	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝑤 ↔ ¬ 𝑧 = 𝑤)
14	13	imbi1i 349	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅))
15		disjabso 45402	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))
16	15	imbi2d 340	. . . . . . . . . . . 12 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
17	14, 16	bitrid 283	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
18	17	imbi2d 340	. . . . . . . . . 10 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
19	12, 18	bitr3id 285	. . . . . . . . 9 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
20	19	ralbidv 3160	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
21	11, 20	bitr3id 285	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
22	21	ralbidva 3158	. . . . . 6 ⊢ (Tr 𝑀 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
23	22	adantr 480	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
24	10, 23	bitrd 279	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
25	6, 24	anbi12d 633	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))))
26		simpl 482	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → Tr 𝑀)
27		elin 3905	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑦) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
28	27	eubii 2585	. . . . . . . 8 ⊢ (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
29		trel 5200	. . . . . . . . . . . 12 ⊢ (Tr 𝑀 → ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀) → 𝑣 ∈ 𝑀))
30	29	imp 406	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀)) → 𝑣 ∈ 𝑀)
31	30	anass1rs 656	. . . . . . . . . 10 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑣 ∈ 𝑦) → 𝑣 ∈ 𝑀)
32	31	adantrl 717	. . . . . . . . 9 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)) → 𝑣 ∈ 𝑀)
33	32	reueubd 3359	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
34	28, 33	bitr4id 290	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
35		reu6 3672	. . . . . . 7 ⊢ (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))
36	34, 35	bitrdi 287	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
37	26, 36	ralabsobidv 45399	. . . . 5 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
38	37	an32s 653	. . . 4 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑦 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
39	38	rexbidva 3159	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
40	25, 39	imbi12d 344	. 2 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))
41	40	ralbidva 3158	1 ⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!weu 2568   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  ∃!wreu 3340   ∩ cin 3888  ∅c0 4273  Tr wtr 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-v 3431  df-dif 3892  df-in 3896  df-ss 3906  df-nul 4274  df-uni 4851  df-tr 5193

This theorem is referenced by:  wfac8prim  45429