Theorem modelac8prim 45436

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

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 45412	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅)))
2		n0abso 45420	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
3	2	adantlr 721	. . . . . . 7 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
4	3	imbi2d 341	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
5	4	ralbidva 3160	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
6	1, 5	bitrd 280	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
7		simpl 483	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → Tr 𝑀)
8		ralabso 45412	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
9	7, 8	ralabsobidv 45416	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
10	9	anabss3 681	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
11		r19.21v 3164	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
12		impexp 451	. . . . . . . . . 10 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
13		df-ne 2935	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝑤 ↔ ¬ 𝑧 = 𝑤)
14	13	imbi1i 350	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅))
15		disjabso 45419	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))
16	15	imbi2d 341	. . . . . . . . . . . 12 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
17	14, 16	bitrid 284	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
18	17	imbi2d 341	. . . . . . . . . 10 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
19	12, 18	bitr3id 286	. . . . . . . . 9 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
20	19	ralbidv 3162	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
21	11, 20	bitr3id 286	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
22	21	ralbidva 3160	. . . . . 6 ⊢ (Tr 𝑀 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
23	22	adantr 481	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
24	10, 23	bitrd 280	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
25	6, 24	anbi12d 638	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))))
26		simpl 483	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → Tr 𝑀)
27		elin 3899	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑦) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
28	27	eubii 2589	. . . . . . . 8 ⊢ (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
29		trel 5187	. . . . . . . . . . . 12 ⊢ (Tr 𝑀 → ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀) → 𝑣 ∈ 𝑀))
30	29	imp 407	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀)) → 𝑣 ∈ 𝑀)
31	30	anass1rs 661	. . . . . . . . . 10 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑣 ∈ 𝑦) → 𝑣 ∈ 𝑀)
32	31	adantrl 722	. . . . . . . . 9 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)) → 𝑣 ∈ 𝑀)
33	32	reueubd 3361	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
34	28, 33	bitr4id 291	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
35		reu6 3667	. . . . . . 7 ⊢ (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))
36	34, 35	bitrdi 288	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
37	26, 36	ralabsobidv 45416	. . . . 5 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
38	37	an32s 658	. . . 4 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑦 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
39	38	rexbidva 3161	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
40	25, 39	imbi12d 345	. 2 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))
41	40	ralbidva 3160	1 ⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃!weu 2572   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  ∃!wreu 3342   ∩ cin 3882  ∅c0 4261  Tr wtr 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-v 3433  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4262  df-uni 4839  df-tr 5180

This theorem is referenced by:  wfac8prim  45446