Theorem modelac8prim 45701

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

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 45677	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅)))
2		n0abso 45685	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
3	2	adantlr 727	. . . . . . 7 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → (𝑧 ≠ ∅ ↔ ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧))
4	3	imbi2d 343	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
5	4	ralbidva 3186	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → 𝑧 ≠ ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
6	1, 5	bitrd 282	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧)))
7		simpl 487	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → Tr 𝑀)
8		ralabso 45677	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
9	7, 8	ralabsobidv 45681	. . . . . 6 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
10	9	anabss3 687	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))))
11		r19.21v 3190	. . . . . . . 8 ⊢ (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
12		impexp 455	. . . . . . . . . 10 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
13		df-ne 2959	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝑤 ↔ ¬ 𝑧 = 𝑤)
14	13	imbi1i 352	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅))
15		disjabso 45684	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))
16	15	imbi2d 343	. . . . . . . . . . . 12 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((¬ 𝑧 = 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
17	14, 16	bitrid 286	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))
18	17	imbi2d 343	. . . . . . . . . 10 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
19	12, 18	bitr3id 288	. . . . . . . . 9 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
20	19	ralbidv 3188	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 (𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
21	11, 20	bitr3id 288	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
22	21	ralbidva 3186	. . . . . 6 ⊢ (Tr 𝑀 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
23	22	adantr 485	. . . . 5 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
24	10, 23	bitrd 282	. . . 4 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))))
25	6, 24	anbi12d 643	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤))))))
26		simpl 487	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → Tr 𝑀)
27		elin 3921	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑦) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
28	27	eubii 2613	. . . . . . . 8 ⊢ (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦))
29		trel 5226	. . . . . . . . . . . 12 ⊢ (Tr 𝑀 → ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀) → 𝑣 ∈ 𝑀))
30	29	imp 411	. . . . . . . . . . 11 ⊢ ((Tr 𝑀 ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀)) → 𝑣 ∈ 𝑀)
31	30	anass1rs 667	. . . . . . . . . 10 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑣 ∈ 𝑦) → 𝑣 ∈ 𝑀)
32	31	adantrl 728	. . . . . . . . 9 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)) → 𝑣 ∈ 𝑀)
33	32	reueubd 3386	. . . . . . . 8 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
34	28, 33	bitr4id 293	. . . . . . 7 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)))
35		reu6 3689	. . . . . . 7 ⊢ (∃!𝑣 ∈ 𝑀 (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))
36	34, 35	bitrdi 290	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
37	26, 36	ralabsobidv 45681	. . . . 5 ⊢ (((Tr 𝑀 ∧ 𝑦 ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
38	37	an32s 664	. . . 4 ⊢ (((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) ∧ 𝑦 ∈ 𝑀) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
39	38	rexbidva 3187	. . 3 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
40	25, 39	imbi12d 347	. 2 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))
41	40	ralbidva 3186	1 ⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃!weu 2596   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  ∃!wreu 3367   ∩ cin 3904  ∅c0 4286  Tr wtr 5218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-v 3457  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287  df-uni 4873  df-tr 5219

This theorem is referenced by:  wfac8prim  45711