Metamath Proof Explorer

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 
|- W = U. ( R1 " On )
Assertion wfac8prim 
|- A. x e. W ( ( A. z e. W ( z e. x -> E. w e. W w e. z ) /\ A. z e. W A. w e. W ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. W ( y e. z -> -. y e. w ) ) ) ) -> E. y e. W A. z e. W ( z e. x -> E. w e. W A. v e. W ( ( v e. z /\ v e. y ) <-> v = w ) ) )

Proof

Step Hyp Ref Expression
1 wfax.1 
 |-  W = U. ( R1 " On )
2 trwf 
 |-  Tr U. ( R1 " On )
3 treq 
 |-  ( W = U. ( R1 " On ) -> ( Tr W <-> Tr U. ( R1 " On ) ) )
4 1 3 ax-mp 
 |-  ( Tr W <-> Tr U. ( R1 " On ) )
5 2 4 mpbir 
 |-  Tr W
6 ac8 
 |-  ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. t A. z e. x E! v v e. ( z i^i t ) )
7 uniwf 
 |-  ( x e. U. ( R1 " On ) <-> U. x e. U. ( R1 " On ) )
8 inss2 
 |-  ( t i^i U. x ) C_ U. x
9 sswf 
 |-  ( ( U. x e. U. ( R1 " On ) /\ ( t i^i U. x ) C_ U. x ) -> ( t i^i U. x ) e. U. ( R1 " On ) )
10 8 9 mpan2 
 |-  ( U. x e. U. ( R1 " On ) -> ( t i^i U. x ) e. U. ( R1 " On ) )
11 7 10 sylbi 
 |-  ( x e. U. ( R1 " On ) -> ( t i^i U. x ) e. U. ( R1 " On ) )
12 1 eleq2i 
 |-  ( x e. W <-> x e. U. ( R1 " On ) )
13 1 eleq2i 
 |-  ( ( t i^i U. x ) e. W <-> ( t i^i U. x ) e. U. ( R1 " On ) )
14 11 12 13 3imtr4i 
 |-  ( x e. W -> ( t i^i U. x ) e. W )
15 inss1 
 |-  ( z i^i t ) C_ z
16 elssuni 
 |-  ( z e. x -> z C_ U. x )
17 15 16 sstrid 
 |-  ( z e. x -> ( z i^i t ) C_ U. x )
18 dfss 
 |-  ( ( z i^i t ) C_ U. x <-> ( z i^i t ) = ( ( z i^i t ) i^i U. x ) )
19 17 18 sylib 
 |-  ( z e. x -> ( z i^i t ) = ( ( z i^i t ) i^i U. x ) )
20 inass 
 |-  ( ( z i^i t ) i^i U. x ) = ( z i^i ( t i^i U. x ) )
21 19 20 eqtrdi 
 |-  ( z e. x -> ( z i^i t ) = ( z i^i ( t i^i U. x ) ) )
22 21 eleq2d 
 |-  ( z e. x -> ( v e. ( z i^i t ) <-> v e. ( z i^i ( t i^i U. x ) ) ) )
23 22 eubidv 
 |-  ( z e. x -> ( E! v v e. ( z i^i t ) <-> E! v v e. ( z i^i ( t i^i U. x ) ) ) )
24 23 ralbiia 
 |-  ( A. z e. x E! v v e. ( z i^i t ) <-> A. z e. x E! v v e. ( z i^i ( t i^i U. x ) ) )
25 ineq2 
 |-  ( y = ( t i^i U. x ) -> ( z i^i y ) = ( z i^i ( t i^i U. x ) ) )
26 25 eleq2d 
 |-  ( y = ( t i^i U. x ) -> ( v e. ( z i^i y ) <-> v e. ( z i^i ( t i^i U. x ) ) ) )
27 26 eubidv 
 |-  ( y = ( t i^i U. x ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i ( t i^i U. x ) ) ) )
28 27 ralbidv 
 |-  ( y = ( t i^i U. x ) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x E! v v e. ( z i^i ( t i^i U. x ) ) ) )
29 28 rspcev 
 |-  ( ( ( t i^i U. x ) e. W /\ A. z e. x E! v v e. ( z i^i ( t i^i U. x ) ) ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) )
30 24 29 sylan2b 
 |-  ( ( ( t i^i U. x ) e. W /\ A. z e. x E! v v e. ( z i^i t ) ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) )
31 14 30 sylan 
 |-  ( ( x e. W /\ A. z e. x E! v v e. ( z i^i t ) ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) )
32 31 ex 
 |-  ( x e. W -> ( A. z e. x E! v v e. ( z i^i t ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) ) )
33 32 exlimdv 
 |-  ( x e. W -> ( E. t A. z e. x E! v v e. ( z i^i t ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) ) )
34 6 33 syl5 
 |-  ( x e. W -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) ) )
35 34 rgen 
 |-  A. x e. W ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) )
36 modelac8prim 
 |-  ( Tr W -> ( A. x e. W ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y e. W A. z e. x E! v v e. ( z i^i y ) ) <-> A. x e. W ( ( A. z e. W ( z e. x -> E. w e. W w e. z ) /\ A. z e. W A. w e. W ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. W ( y e. z -> -. y e. w ) ) ) ) -> E. y e. W A. z e. W ( z e. x -> E. w e. W A. v e. W ( ( v e. z /\ v e. y ) <-> v = w ) ) ) ) )
37 35 36 mpbii 
 |-  ( Tr W -> A. x e. W ( ( A. z e. W ( z e. x -> E. w e. W w e. z ) /\ A. z e. W A. w e. W ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. W ( y e. z -> -. y e. w ) ) ) ) -> E. y e. W A. z e. W ( z e. x -> E. w e. W A. v e. W ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
38 5 37 ax-mp 
 |-  A. x e. W ( ( A. z e. W ( z e. x -> E. w e. W w e. z ) /\ A. z e. W A. w e. W ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y e. W ( y e. z -> -. y e. w ) ) ) ) -> E. y e. W A. z e. W ( z e. x -> E. w e. W A. v e. W ( ( v e. z /\ v e. y ) <-> v = w ) ) )