Theorem wfac8prim 44992

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

Hypothesis

Ref	Expression
wfax.1	⊢ 𝑊 = ∪ (𝑅1 “ On)

Assertion

Ref	Expression
wfac8prim	⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑊

Proof of Theorem wfac8prim

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		trwf 44951	. . 3 ⊢ Tr ∪ (𝑅1 “ On)
2		wfax.1	. . . 4 ⊢ 𝑊 = ∪ (𝑅1 “ On)
3		treq 5265	. . . 4 ⊢ (𝑊 = ∪ (𝑅1 “ On) → (Tr 𝑊 ↔ Tr ∪ (𝑅1 “ On)))
4	2, 3	ax-mp 5	. . 3 ⊢ (Tr 𝑊 ↔ Tr ∪ (𝑅1 “ On))
5	1, 4	mpbir 231	. 2 ⊢ Tr 𝑊
6		ac8 10528	. . . . 5 ⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑡∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡))
7		uniwf 9855	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝑥 ∈ ∪ (𝑅1 “ On))
8		inss2 4237	. . . . . . . . . . 11 ⊢ (𝑡 ∩ ∪ 𝑥) ⊆ ∪ 𝑥
9		sswf 9844	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ∈ ∪ (𝑅1 “ On) ∧ (𝑡 ∩ ∪ 𝑥) ⊆ ∪ 𝑥) → (𝑡 ∩ ∪ 𝑥) ∈ ∪ (𝑅1 “ On))
10	8, 9	mpan2 691	. . . . . . . . . 10 ⊢ (∪ 𝑥 ∈ ∪ (𝑅1 “ On) → (𝑡 ∩ ∪ 𝑥) ∈ ∪ (𝑅1 “ On))
11	7, 10	sylbi 217	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → (𝑡 ∩ ∪ 𝑥) ∈ ∪ (𝑅1 “ On))
12	2	eleq2i 2832	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ∪ (𝑅1 “ On))
13	2	eleq2i 2832	. . . . . . . . 9 ⊢ ((𝑡 ∩ ∪ 𝑥) ∈ 𝑊 ↔ (𝑡 ∩ ∪ 𝑥) ∈ ∪ (𝑅1 “ On))
14	11, 12, 13	3imtr4i 292	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑊 → (𝑡 ∩ ∪ 𝑥) ∈ 𝑊)
15		inss1 4236	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∩ 𝑡) ⊆ 𝑧
16		elssuni 4935	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑥 → 𝑧 ⊆ ∪ 𝑥)
17	15, 16	sstrid 3994	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ 𝑡) ⊆ ∪ 𝑥)
18		dfss 3969	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∩ 𝑡) ⊆ ∪ 𝑥 ↔ (𝑧 ∩ 𝑡) = ((𝑧 ∩ 𝑡) ∩ ∪ 𝑥))
19	17, 18	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ 𝑡) = ((𝑧 ∩ 𝑡) ∩ ∪ 𝑥))
20		inass 4227	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∩ 𝑡) ∩ ∪ 𝑥) = (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))
21	19, 20	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ 𝑡) = (𝑧 ∩ (𝑡 ∩ ∪ 𝑥)))
22	21	eleq2d 2826	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑥 → (𝑣 ∈ (𝑧 ∩ 𝑡) ↔ 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))))
23	22	eubidv 2585	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑥 → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡) ↔ ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))))
24	23	ralbiia 3090	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡) ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥)))
25		ineq2 4213	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑡 ∩ ∪ 𝑥) → (𝑧 ∩ 𝑦) = (𝑧 ∩ (𝑡 ∩ ∪ 𝑥)))
26	25	eleq2d 2826	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑡 ∩ ∪ 𝑥) → (𝑣 ∈ (𝑧 ∩ 𝑦) ↔ 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))))
27	26	eubidv 2585	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑡 ∩ ∪ 𝑥) → (∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))))
28	27	ralbidv 3177	. . . . . . . . . 10 ⊢ (𝑦 = (𝑡 ∩ ∪ 𝑥) → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))))
29	28	rspcev 3621	. . . . . . . . 9 ⊢ (((𝑡 ∩ ∪ 𝑥) ∈ 𝑊 ∧ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑡 ∩ ∪ 𝑥))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))
30	24, 29	sylan2b 594	. . . . . . . 8 ⊢ (((𝑡 ∩ ∪ 𝑥) ∈ 𝑊 ∧ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡)) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))
31	14, 30	sylan 580	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑊 ∧ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡)) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))
32	31	ex 412	. . . . . 6 ⊢ (𝑥 ∈ 𝑊 → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
33	32	exlimdv 1933	. . . . 5 ⊢ (𝑥 ∈ 𝑊 → (∃𝑡∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑡) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
34	6, 33	syl5 34	. . . 4 ⊢ (𝑥 ∈ 𝑊 → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
35	34	rgen 3062	. . 3 ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))
36		modelac8prim 44982	. . 3 ⊢ (Tr 𝑊 → (∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))
37	35, 36	mpbii 233	. 2 ⊢ (Tr 𝑊 → ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
38	5, 37	ax-mp 5	1 ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃!weu 2567   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ∩ cin 3949   ⊆ wss 3950  ∅c0 4332  ∪ cuni 4905  Tr wtr 5257   “ cima 5686  Oncon0 6382  𝑅₁cr1 9798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-ac2 10499

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-int 4945  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-ov 7432  df-om 7884  df-2nd 8011  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-r1 9800  df-rank 9801  df-ac 10152

This theorem is referenced by: (None)