Metamath Proof Explorer

Theorem permac8prim

Description: The Axiom of Choice ac8prim holds in permutation models. Part of Exercise II.9.3 of Kunen2 p. 149. Note that ax-ac requires Regularity for its derivation from the usual Axiom of Choice and does not necessarily hold in permutation models. (Contributed by Eric Schmidt, 16-Nov-2025)

Ref Expression
Hypotheses permmodel.1 
|- F : _V -1-1-onto-> _V
permmodel.2 
|- R = ( `' F o. _E )
Assertion permac8prim 
|- ( ( A. z ( z R x -> E. w w R z ) /\ A. z A. w ( ( z R x /\ w R x ) -> ( -. z = w -> A. y ( y R z -> -. y R w ) ) ) ) -> E. y A. z ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) )

Proof

Step Hyp Ref Expression
1 permmodel.1 
 |-  F : _V -1-1-onto-> _V
2 permmodel.2 
 |-  R = ( `' F o. _E )
3 df-ral 
 |-  ( A. z e. ( F ` x ) ( F ` z ) =/= (/) <-> A. z ( z e. ( F ` x ) -> ( F ` z ) =/= (/) ) )
4 f1ofn 
 |-  ( F : _V -1-1-onto-> _V -> F Fn _V )
5 1 4 ax-mp 
 |-  F Fn _V
6 ssv 
 |-  ( F ` x ) C_ _V
7 neeq1 
 |-  ( t = ( F ` z ) -> ( t =/= (/) <-> ( F ` z ) =/= (/) ) )
8 7 ralima 
 |-  ( ( F Fn _V /\ ( F ` x ) C_ _V ) -> ( A. t e. ( F " ( F ` x ) ) t =/= (/) <-> A. z e. ( F ` x ) ( F ` z ) =/= (/) ) )
9 5 6 8 mp2an 
 |-  ( A. t e. ( F " ( F ` x ) ) t =/= (/) <-> A. z e. ( F ` x ) ( F ` z ) =/= (/) )
10 vex 
 |-  z e. _V
11 vex 
 |-  x e. _V
12 1 2 10 11 brpermmodel 
 |-  ( z R x <-> z e. ( F ` x ) )
13 vex 
 |-  w e. _V
14 1 2 13 10 brpermmodel 
 |-  ( w R z <-> w e. ( F ` z ) )
15 14 exbii 
 |-  ( E. w w R z <-> E. w w e. ( F ` z ) )
16 n0 
 |-  ( ( F ` z ) =/= (/) <-> E. w w e. ( F ` z ) )
17 15 16 bitr4i 
 |-  ( E. w w R z <-> ( F ` z ) =/= (/) )
18 12 17 imbi12i 
 |-  ( ( z R x -> E. w w R z ) <-> ( z e. ( F ` x ) -> ( F ` z ) =/= (/) ) )
19 18 albii 
 |-  ( A. z ( z R x -> E. w w R z ) <-> A. z ( z e. ( F ` x ) -> ( F ` z ) =/= (/) ) )
20 3 9 19 3bitr4i 
 |-  ( A. t e. ( F " ( F ` x ) ) t =/= (/) <-> A. z ( z R x -> E. w w R z ) )
21 neeq2 
 |-  ( q = ( F ` w ) -> ( t =/= q <-> t =/= ( F ` w ) ) )
22 ineq2 
 |-  ( q = ( F ` w ) -> ( t i^i q ) = ( t i^i ( F ` w ) ) )
23 22 eqeq1d 
 |-  ( q = ( F ` w ) -> ( ( t i^i q ) = (/) <-> ( t i^i ( F ` w ) ) = (/) ) )
24 21 23 imbi12d 
 |-  ( q = ( F ` w ) -> ( ( t =/= q -> ( t i^i q ) = (/) ) <-> ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) ) )
25 24 ralima 
 |-  ( ( F Fn _V /\ ( F ` x ) C_ _V ) -> ( A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) <-> A. w e. ( F ` x ) ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) ) )
26 5 6 25 mp2an 
 |-  ( A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) <-> A. w e. ( F ` x ) ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) )
27 26 ralbii 
 |-  ( A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) <-> A. t e. ( F " ( F ` x ) ) A. w e. ( F ` x ) ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) )
28 neeq1 
 |-  ( t = ( F ` z ) -> ( t =/= ( F ` w ) <-> ( F ` z ) =/= ( F ` w ) ) )
29 ineq1 
 |-  ( t = ( F ` z ) -> ( t i^i ( F ` w ) ) = ( ( F ` z ) i^i ( F ` w ) ) )
30 29 eqeq1d 
 |-  ( t = ( F ` z ) -> ( ( t i^i ( F ` w ) ) = (/) <-> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) )
31 28 30 imbi12d 
 |-  ( t = ( F ` z ) -> ( ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) <-> ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
32 31 ralbidv 
 |-  ( t = ( F ` z ) -> ( A. w e. ( F ` x ) ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) <-> A. w e. ( F ` x ) ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
33 32 ralima 
 |-  ( ( F Fn _V /\ ( F ` x ) C_ _V ) -> ( A. t e. ( F " ( F ` x ) ) A. w e. ( F ` x ) ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) <-> A. z e. ( F ` x ) A. w e. ( F ` x ) ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
34 5 6 33 mp2an 
 |-  ( A. t e. ( F " ( F ` x ) ) A. w e. ( F ` x ) ( t =/= ( F ` w ) -> ( t i^i ( F ` w ) ) = (/) ) <-> A. z e. ( F ` x ) A. w e. ( F ` x ) ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) )
35 r2al 
 |-  ( A. z e. ( F ` x ) A. w e. ( F ` x ) ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) <-> A. z A. w ( ( z e. ( F ` x ) /\ w e. ( F ` x ) ) -> ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
36 27 34 35 3bitri 
 |-  ( A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) <-> A. z A. w ( ( z e. ( F ` x ) /\ w e. ( F ` x ) ) -> ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
37 1 2 13 11 brpermmodel 
 |-  ( w R x <-> w e. ( F ` x ) )
38 12 37 anbi12i 
 |-  ( ( z R x /\ w R x ) <-> ( z e. ( F ` x ) /\ w e. ( F ` x ) ) )
39 df-ne 
 |-  ( ( F ` z ) =/= ( F ` w ) <-> -. ( F ` z ) = ( F ` w ) )
40 f1of1 
 |-  ( F : _V -1-1-onto-> _V -> F : _V -1-1-> _V )
41 1 40 ax-mp 
 |-  F : _V -1-1-> _V
42 f1fveq 
 |-  ( ( F : _V -1-1-> _V /\ ( z e. _V /\ w e. _V ) ) -> ( ( F ` z ) = ( F ` w ) <-> z = w ) )
43 41 42 mpan 
 |-  ( ( z e. _V /\ w e. _V ) -> ( ( F ` z ) = ( F ` w ) <-> z = w ) )
44 43 el2v 
 |-  ( ( F ` z ) = ( F ` w ) <-> z = w )
45 44 notbii 
 |-  ( -. ( F ` z ) = ( F ` w ) <-> -. z = w )
46 39 45 bitr2i 
 |-  ( -. z = w <-> ( F ` z ) =/= ( F ` w ) )
47 vex 
 |-  y e. _V
48 1 2 47 10 brpermmodel 
 |-  ( y R z <-> y e. ( F ` z ) )
49 1 2 47 13 brpermmodel 
 |-  ( y R w <-> y e. ( F ` w ) )
50 49 notbii 
 |-  ( -. y R w <-> -. y e. ( F ` w ) )
51 48 50 imbi12i 
 |-  ( ( y R z -> -. y R w ) <-> ( y e. ( F ` z ) -> -. y e. ( F ` w ) ) )
52 51 albii 
 |-  ( A. y ( y R z -> -. y R w ) <-> A. y ( y e. ( F ` z ) -> -. y e. ( F ` w ) ) )
53 disj1 
 |-  ( ( ( F ` z ) i^i ( F ` w ) ) = (/) <-> A. y ( y e. ( F ` z ) -> -. y e. ( F ` w ) ) )
54 52 53 bitr4i 
 |-  ( A. y ( y R z -> -. y R w ) <-> ( ( F ` z ) i^i ( F ` w ) ) = (/) )
55 46 54 imbi12i 
 |-  ( ( -. z = w -> A. y ( y R z -> -. y R w ) ) <-> ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) )
56 38 55 imbi12i 
 |-  ( ( ( z R x /\ w R x ) -> ( -. z = w -> A. y ( y R z -> -. y R w ) ) ) <-> ( ( z e. ( F ` x ) /\ w e. ( F ` x ) ) -> ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
57 56 2albii 
 |-  ( A. z A. w ( ( z R x /\ w R x ) -> ( -. z = w -> A. y ( y R z -> -. y R w ) ) ) <-> A. z A. w ( ( z e. ( F ` x ) /\ w e. ( F ` x ) ) -> ( ( F ` z ) =/= ( F ` w ) -> ( ( F ` z ) i^i ( F ` w ) ) = (/) ) ) )
58 36 57 bitr4i 
 |-  ( A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) <-> A. z A. w ( ( z R x /\ w R x ) -> ( -. z = w -> A. y ( y R z -> -. y R w ) ) ) )
59 f1ofun 
 |-  ( F : _V -1-1-onto-> _V -> Fun F )
60 fvex 
 |-  ( F ` x ) e. _V
61 60 funimaex 
 |-  ( Fun F -> ( F " ( F ` x ) ) e. _V )
62 1 59 61 mp2b 
 |-  ( F " ( F ` x ) ) e. _V
63 raleq 
 |-  ( r = ( F " ( F ` x ) ) -> ( A. t e. r t =/= (/) <-> A. t e. ( F " ( F ` x ) ) t =/= (/) ) )
64 raleq 
 |-  ( r = ( F " ( F ` x ) ) -> ( A. q e. r ( t =/= q -> ( t i^i q ) = (/) ) <-> A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) ) )
65 64 raleqbi1dv 
 |-  ( r = ( F " ( F ` x ) ) -> ( A. t e. r A. q e. r ( t =/= q -> ( t i^i q ) = (/) ) <-> A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) ) )
66 63 65 anbi12d 
 |-  ( r = ( F " ( F ` x ) ) -> ( ( A. t e. r t =/= (/) /\ A. t e. r A. q e. r ( t =/= q -> ( t i^i q ) = (/) ) ) <-> ( A. t e. ( F " ( F ` x ) ) t =/= (/) /\ A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) ) ) )
67 raleq 
 |-  ( r = ( F " ( F ` x ) ) -> ( A. t e. r E! v v e. ( t i^i s ) <-> A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) ) )
68 67 exbidv 
 |-  ( r = ( F " ( F ` x ) ) -> ( E. s A. t e. r E! v v e. ( t i^i s ) <-> E. s A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) ) )
69 66 68 imbi12d 
 |-  ( r = ( F " ( F ` x ) ) -> ( ( ( A. t e. r t =/= (/) /\ A. t e. r A. q e. r ( t =/= q -> ( t i^i q ) = (/) ) ) -> E. s A. t e. r E! v v e. ( t i^i s ) ) <-> ( ( A. t e. ( F " ( F ` x ) ) t =/= (/) /\ A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) ) -> E. s A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) ) ) )
70 ac8 
 |-  ( ( A. t e. r t =/= (/) /\ A. t e. r A. q e. r ( t =/= q -> ( t i^i q ) = (/) ) ) -> E. s A. t e. r E! v v e. ( t i^i s ) )
71 62 69 70 vtocl 
 |-  ( ( A. t e. ( F " ( F ` x ) ) t =/= (/) /\ A. t e. ( F " ( F ` x ) ) A. q e. ( F " ( F ` x ) ) ( t =/= q -> ( t i^i q ) = (/) ) ) -> E. s A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) )
72 20 58 71 syl2anbr 
 |-  ( ( A. z ( z R x -> E. w w R z ) /\ A. z A. w ( ( z R x /\ w R x ) -> ( -. z = w -> A. y ( y R z -> -. y R w ) ) ) ) -> E. s A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) )
73 ineq1 
 |-  ( t = ( F ` z ) -> ( t i^i s ) = ( ( F ` z ) i^i s ) )
74 73 eleq2d 
 |-  ( t = ( F ` z ) -> ( v e. ( t i^i s ) <-> v e. ( ( F ` z ) i^i s ) ) )
75 74 eubidv 
 |-  ( t = ( F ` z ) -> ( E! v v e. ( t i^i s ) <-> E! v v e. ( ( F ` z ) i^i s ) ) )
76 75 ralima 
 |-  ( ( F Fn _V /\ ( F ` x ) C_ _V ) -> ( A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) <-> A. z e. ( F ` x ) E! v v e. ( ( F ` z ) i^i s ) ) )
77 5 6 76 mp2an 
 |-  ( A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) <-> A. z e. ( F ` x ) E! v v e. ( ( F ` z ) i^i s ) )
78 df-ral 
 |-  ( A. z e. ( F ` x ) E! v v e. ( ( F ` z ) i^i s ) <-> A. z ( z e. ( F ` x ) -> E! v v e. ( ( F ` z ) i^i s ) ) )
79 77 78 bitri 
 |-  ( A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) <-> A. z ( z e. ( F ` x ) -> E! v v e. ( ( F ` z ) i^i s ) ) )
80 fvex 
 |-  ( `' F ` s ) e. _V
81 12 a1i 
 |-  ( y = ( `' F ` s ) -> ( z R x <-> z e. ( F ` x ) ) )
82 vex 
 |-  v e. _V
83 1 2 82 10 brpermmodel 
 |-  ( v R z <-> v e. ( F ` z ) )
84 83 a1i 
 |-  ( y = ( `' F ` s ) -> ( v R z <-> v e. ( F ` z ) ) )
85 breq2 
 |-  ( y = ( `' F ` s ) -> ( v R y <-> v R ( `' F ` s ) ) )
86 vex 
 |-  s e. _V
87 1 2 82 86 brpermmodelcnv 
 |-  ( v R ( `' F ` s ) <-> v e. s )
88 85 87 bitrdi 
 |-  ( y = ( `' F ` s ) -> ( v R y <-> v e. s ) )
89 84 88 anbi12d 
 |-  ( y = ( `' F ` s ) -> ( ( v R z /\ v R y ) <-> ( v e. ( F ` z ) /\ v e. s ) ) )
90 89 bibi1d 
 |-  ( y = ( `' F ` s ) -> ( ( ( v R z /\ v R y ) <-> v = w ) <-> ( ( v e. ( F ` z ) /\ v e. s ) <-> v = w ) ) )
91 90 albidv 
 |-  ( y = ( `' F ` s ) -> ( A. v ( ( v R z /\ v R y ) <-> v = w ) <-> A. v ( ( v e. ( F ` z ) /\ v e. s ) <-> v = w ) ) )
92 91 exbidv 
 |-  ( y = ( `' F ` s ) -> ( E. w A. v ( ( v R z /\ v R y ) <-> v = w ) <-> E. w A. v ( ( v e. ( F ` z ) /\ v e. s ) <-> v = w ) ) )
93 elin 
 |-  ( v e. ( ( F ` z ) i^i s ) <-> ( v e. ( F ` z ) /\ v e. s ) )
94 93 eubii 
 |-  ( E! v v e. ( ( F ` z ) i^i s ) <-> E! v ( v e. ( F ` z ) /\ v e. s ) )
95 eu6 
 |-  ( E! v ( v e. ( F ` z ) /\ v e. s ) <-> E. w A. v ( ( v e. ( F ` z ) /\ v e. s ) <-> v = w ) )
96 94 95 bitri 
 |-  ( E! v v e. ( ( F ` z ) i^i s ) <-> E. w A. v ( ( v e. ( F ` z ) /\ v e. s ) <-> v = w ) )
97 92 96 bitr4di 
 |-  ( y = ( `' F ` s ) -> ( E. w A. v ( ( v R z /\ v R y ) <-> v = w ) <-> E! v v e. ( ( F ` z ) i^i s ) ) )
98 81 97 imbi12d 
 |-  ( y = ( `' F ` s ) -> ( ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) <-> ( z e. ( F ` x ) -> E! v v e. ( ( F ` z ) i^i s ) ) ) )
99 98 albidv 
 |-  ( y = ( `' F ` s ) -> ( A. z ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) <-> A. z ( z e. ( F ` x ) -> E! v v e. ( ( F ` z ) i^i s ) ) ) )
100 80 99 spcev 
 |-  ( A. z ( z e. ( F ` x ) -> E! v v e. ( ( F ` z ) i^i s ) ) -> E. y A. z ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) )
101 79 100 sylbi 
 |-  ( A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) -> E. y A. z ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) )
102 101 exlimiv 
 |-  ( E. s A. t e. ( F " ( F ` x ) ) E! v v e. ( t i^i s ) -> E. y A. z ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) )
103 72 102 syl 
 |-  ( ( A. z ( z R x -> E. w w R z ) /\ A. z A. w ( ( z R x /\ w R x ) -> ( -. z = w -> A. y ( y R z -> -. y R w ) ) ) ) -> E. y A. z ( z R x -> E. w A. v ( ( v R z /\ v R y ) <-> v = w ) ) )