Description: The Null Set Axiom ax-nul holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | permmodel.1 | |- F : _V -1-1-onto-> _V |
|
| permmodel.2 | |- R = ( `' F o. _E ) |
||
| Assertion | permaxnul | |- E. x A. y -. y R x |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | permmodel.1 | |- F : _V -1-1-onto-> _V |
|
| 2 | permmodel.2 | |- R = ( `' F o. _E ) |
|
| 3 | fvex | |- ( `' F ` (/) ) e. _V |
|
| 4 | breq2 | |- ( x = ( `' F ` (/) ) -> ( y R x <-> y R ( `' F ` (/) ) ) ) |
|
| 5 | 4 | notbid | |- ( x = ( `' F ` (/) ) -> ( -. y R x <-> -. y R ( `' F ` (/) ) ) ) |
| 6 | 5 | albidv | |- ( x = ( `' F ` (/) ) -> ( A. y -. y R x <-> A. y -. y R ( `' F ` (/) ) ) ) |
| 7 | noel | |- -. y e. (/) |
|
| 8 | vex | |- y e. _V |
|
| 9 | 0ex | |- (/) e. _V |
|
| 10 | 1 2 8 9 | brpermmodelcnv | |- ( y R ( `' F ` (/) ) <-> y e. (/) ) |
| 11 | 7 10 | mtbir | |- -. y R ( `' F ` (/) ) |
| 12 | 11 | ax-gen | |- A. y -. y R ( `' F ` (/) ) |
| 13 | 3 6 12 | ceqsexv2d | |- E. x A. y -. y R x |