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 -> ( A. x e. M ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y e. M A. z e. x E! v v e. ( z i^i y ) ) <-> A. x e. M ( ( A. z e. M ( z e. x -> E. w e. M w e. z ) /\ A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) -> E. y e. M A. z e. M ( z e. x -> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralabso	|- ( ( Tr M /\ x e. M ) -> ( A. z e. x z =/= (/) <-> A. z e. M ( z e. x -> z =/= (/) ) ) )
2		n0abso	|- ( ( Tr M /\ z e. M ) -> ( z =/= (/) <-> E. w e. M w e. z ) )
3	2	adantlr	|- ( ( ( Tr M /\ x e. M ) /\ z e. M ) -> ( z =/= (/) <-> E. w e. M w e. z ) )
4	3	imbi2d	|- ( ( ( Tr M /\ x e. M ) /\ z e. M ) -> ( ( z e. x -> z =/= (/) ) <-> ( z e. x -> E. w e. M w e. z ) ) )
5	4	ralbidva	|- ( ( Tr M /\ x e. M ) -> ( A. z e. M ( z e. x -> z =/= (/) ) <-> A. z e. M ( z e. x -> E. w e. M w e. z ) ) )
6	1 5	bitrd	|- ( ( Tr M /\ x e. M ) -> ( A. z e. x z =/= (/) <-> A. z e. M ( z e. x -> E. w e. M w e. z ) ) )
7		simpl	|- ( ( Tr M /\ x e. M ) -> Tr M )
8		ralabso	|- ( ( Tr M /\ x e. M ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) )
9	7 8	ralabsobidv	|- ( ( ( Tr M /\ x e. M ) /\ x e. M ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. M ( z e. x -> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) ) )
10	9	anabss3	|- ( ( Tr M /\ x e. M ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. M ( z e. x -> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) ) )
11		r19.21v	|- ( A. w e. M ( z e. x -> ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) <-> ( z e. x -> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) )
12		impexp	|- ( ( ( z e. x /\ w e. x ) -> ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( z e. x -> ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) )
13		df-ne	|- ( z =/= w <-> -. z = w )
14	13	imbi1i	|- ( ( z =/= w -> ( z i^i w ) = (/) ) <-> ( -. z = w -> ( z i^i w ) = (/) ) )
15		disjabso	|- ( ( Tr M /\ z e. M ) -> ( ( z i^i w ) = (/) <-> A. y e. M ( y e. z -> -. y e. w ) ) )
16	15	imbi2d	|- ( ( Tr M /\ z e. M ) -> ( ( -. z = w -> ( z i^i w ) = (/) ) <-> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) )
17	14 16	bitrid	|- ( ( Tr M /\ z e. M ) -> ( ( z =/= w -> ( z i^i w ) = (/) ) <-> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) )
18	17	imbi2d	|- ( ( Tr M /\ z e. M ) -> ( ( ( z e. x /\ w e. x ) -> ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
19	12 18	bitr3id	|- ( ( Tr M /\ z e. M ) -> ( ( z e. x -> ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) <-> ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
20	19	ralbidv	|- ( ( Tr M /\ z e. M ) -> ( A. w e. M ( z e. x -> ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) <-> A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
21	11 20	bitr3id	|- ( ( Tr M /\ z e. M ) -> ( ( z e. x -> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) <-> A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
22	21	ralbidva	|- ( Tr M -> ( A. z e. M ( z e. x -> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) <-> A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
23	22	adantr	|- ( ( Tr M /\ x e. M ) -> ( A. z e. M ( z e. x -> A. w e. M ( w e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) ) <-> A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
24	10 23	bitrd	|- ( ( Tr M /\ x e. M ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) )
25	6 24	anbi12d	|- ( ( Tr M /\ x e. M ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( A. z e. M ( z e. x -> E. w e. M w e. z ) /\ A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) ) )
26		simpl	|- ( ( Tr M /\ y e. M ) -> Tr M )
27		elin	|- ( v e. ( z i^i y ) <-> ( v e. z /\ v e. y ) )
28	27	eubii	|- ( E! v v e. ( z i^i y ) <-> E! v ( v e. z /\ v e. y ) )
29		trel	|- ( Tr M -> ( ( v e. y /\ y e. M ) -> v e. M ) )
30	29	imp	|- ( ( Tr M /\ ( v e. y /\ y e. M ) ) -> v e. M )
31	30	anass1rs	|- ( ( ( Tr M /\ y e. M ) /\ v e. y ) -> v e. M )
32	31	adantrl	|- ( ( ( Tr M /\ y e. M ) /\ ( v e. z /\ v e. y ) ) -> v e. M )
33	32	reueubd	|- ( ( Tr M /\ y e. M ) -> ( E! v e. M ( v e. z /\ v e. y ) <-> E! v ( v e. z /\ v e. y ) ) )
34	28 33	bitr4id	|- ( ( Tr M /\ y e. M ) -> ( E! v v e. ( z i^i y ) <-> E! v e. M ( v e. z /\ v e. y ) ) )
35		reu6	|- ( E! v e. M ( v e. z /\ v e. y ) <-> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) )
36	34 35	bitrdi	|- ( ( Tr M /\ y e. M ) -> ( E! v v e. ( z i^i y ) <-> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) )
37	26 36	ralabsobidv	|- ( ( ( Tr M /\ y e. M ) /\ x e. M ) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. M ( z e. x -> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
38	37	an32s	|- ( ( ( Tr M /\ x e. M ) /\ y e. M ) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. M ( z e. x -> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
39	38	rexbidva	|- ( ( Tr M /\ x e. M ) -> ( E. y e. M A. z e. x E! v v e. ( z i^i y ) <-> E. y e. M A. z e. M ( z e. x -> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
40	25 39	imbi12d	|- ( ( Tr M /\ x e. M ) -> ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y e. M A. z e. x E! v v e. ( z i^i y ) ) <-> ( ( A. z e. M ( z e. x -> E. w e. M w e. z ) /\ A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) -> E. y e. M A. z e. M ( z e. x -> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) ) ) )
41	40	ralbidva	|- ( Tr M -> ( A. x e. M ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y e. M A. z e. x E! v v e. ( z i^i y ) ) <-> A. x e. M ( ( A. z e. M ( z e. x -> E. w e. M w e. z ) /\ A. z e. M A. w e. M ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. M ( y e. z -> -. y e. w ) ) ) ) -> E. y e. M A. z e. M ( z e. x -> E. w e. M A. v e. M ( ( v e. z /\ v e. y ) <-> v = w ) ) ) ) )