Theorem wfac8prim

Description: The class of well-founded sets W models the Axiom of Choice. Since the previous theorems show that all the ZF axioms hold in W , we may use any statement that ZF proves is equivalent to Choice to prove this. We use ac8prim . Part of Corollary II.2.12 of Kunen2 p. 114. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypothesis	wfax.1	⊢ 𝑊 = ∪ ( 𝑅1 “ On )
Assertion	wfac8prim	⊢ ∀ 𝑥 ∈ 𝑊 ( ( ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∈ 𝑊 ∀ 𝑤 ∈ 𝑊 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ∈ 𝑊 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 ∀ 𝑣 ∈ 𝑊 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfax.1	⊢ 𝑊 = ∪ ( 𝑅1 “ On )
2		trwf	⊢ Tr ∪ ( 𝑅1 “ On )
3		treq	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ( Tr 𝑊 ↔ Tr ∪ ( 𝑅1 “ On ) ) )
4	1 3	ax-mp	⊢ ( Tr 𝑊 ↔ Tr ∪ ( 𝑅1 “ On ) )
5	2 4	mpbir	⊢ Tr 𝑊
6		ac8	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑡 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) )
7		uniwf	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
8		inss2	⊢ ( 𝑡 ∩ ∪ 𝑥 ) ⊆ ∪ 𝑥
9		sswf	⊢ ( ( ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑡 ∩ ∪ 𝑥 ) ⊆ ∪ 𝑥 ) → ( 𝑡 ∩ ∪ 𝑥 ) ∈ ∪ ( 𝑅1 “ On ) )
10	8 9	mpan2	⊢ ( ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑡 ∩ ∪ 𝑥 ) ∈ ∪ ( 𝑅1 “ On ) )
11	7 10	sylbi	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑡 ∩ ∪ 𝑥 ) ∈ ∪ ( 𝑅1 “ On ) )
12	1	eleq2i	⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
13	1	eleq2i	⊢ ( ( 𝑡 ∩ ∪ 𝑥 ) ∈ 𝑊 ↔ ( 𝑡 ∩ ∪ 𝑥 ) ∈ ∪ ( 𝑅1 “ On ) )
14	11 12 13	3imtr4i	⊢ ( 𝑥 ∈ 𝑊 → ( 𝑡 ∩ ∪ 𝑥 ) ∈ 𝑊 )
15		inss1	⊢ ( 𝑧 ∩ 𝑡 ) ⊆ 𝑧
16		elssuni	⊢ ( 𝑧 ∈ 𝑥 → 𝑧 ⊆ ∪ 𝑥 )
17	15 16	sstrid	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ 𝑡 ) ⊆ ∪ 𝑥 )
18		dfss	⊢ ( ( 𝑧 ∩ 𝑡 ) ⊆ ∪ 𝑥 ↔ ( 𝑧 ∩ 𝑡 ) = ( ( 𝑧 ∩ 𝑡 ) ∩ ∪ 𝑥 ) )
19	17 18	sylib	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ 𝑡 ) = ( ( 𝑧 ∩ 𝑡 ) ∩ ∪ 𝑥 ) )
20		inass	⊢ ( ( 𝑧 ∩ 𝑡 ) ∩ ∪ 𝑥 ) = ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) )
21	19 20	eqtrdi	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ 𝑡 ) = ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) )
22	21	eleq2d	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) ) )
23	22	eubidv	⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) ) )
24	23	ralbiia	⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) )
25		ineq2	⊢ ( 𝑦 = ( 𝑡 ∩ ∪ 𝑥 ) → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) )
26	25	eleq2d	⊢ ( 𝑦 = ( 𝑡 ∩ ∪ 𝑥 ) → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) ) )
27	26	eubidv	⊢ ( 𝑦 = ( 𝑡 ∩ ∪ 𝑥 ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) ) )
28	27	ralbidv	⊢ ( 𝑦 = ( 𝑡 ∩ ∪ 𝑥 ) → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) ) )
29	28	rspcev	⊢ ( ( ( 𝑡 ∩ ∪ 𝑥 ) ∈ 𝑊 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑡 ∩ ∪ 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
30	24 29	sylan2b	⊢ ( ( ( 𝑡 ∩ ∪ 𝑥 ) ∈ 𝑊 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
31	14 30	sylan	⊢ ( ( 𝑥 ∈ 𝑊 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
32	31	ex	⊢ ( 𝑥 ∈ 𝑊 → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
33	32	exlimdv	⊢ ( 𝑥 ∈ 𝑊 → ( ∃ 𝑡 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑡 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
34	6 33	syl5	⊢ ( 𝑥 ∈ 𝑊 → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
35	34	rgen	⊢ ∀ 𝑥 ∈ 𝑊 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
36		modelac8prim	⊢ ( Tr 𝑊 → ( ∀ 𝑥 ∈ 𝑊 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑊 ( ( ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∈ 𝑊 ∀ 𝑤 ∈ 𝑊 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ∈ 𝑊 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 ∀ 𝑣 ∈ 𝑊 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) ) )
37	35 36	mpbii	⊢ ( Tr 𝑊 → ∀ 𝑥 ∈ 𝑊 ( ( ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∈ 𝑊 ∀ 𝑤 ∈ 𝑊 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ∈ 𝑊 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 ∀ 𝑣 ∈ 𝑊 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) )
38	5 37	ax-mp	⊢ ∀ 𝑥 ∈ 𝑊 ( ( ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∈ 𝑊 ∀ 𝑤 ∈ 𝑊 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ∈ 𝑊 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝑊 ∀ 𝑣 ∈ 𝑊 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )