Metamath Proof Explorer

Theorem mh-infprim1bi

Description: Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf or ax-inf2 from this axiom requires ax-ext , ax-rep , and ax-reg , see inf3 and inf0 . (Contributed by Matthew House, 13-Apr-2026)

Ref Expression
Assertion mh-infprim1bi 
|- ( E. x ( x =/= (/) /\ x C_ U. x ) <-> -. A. x -. A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )

Proof

Step Hyp Ref Expression
1 exnelv 
 |-  E. y -. y e. x
2 1 a1bi 
 |-  ( x =/= (/) <-> ( E. y -. y e. x -> x =/= (/) ) )
3 19.23v 
 |-  ( A. y ( -. y e. x -> x =/= (/) ) <-> ( E. y -. y e. x -> x =/= (/) ) )
4 n0 
 |-  ( x =/= (/) <-> E. z z e. x )
5 pm2.21 
 |-  ( -. y e. x -> ( y e. x -> y e. z ) )
6 5 biantrurd 
 |-  ( -. y e. x -> ( z e. x <-> ( ( y e. x -> y e. z ) /\ z e. x ) ) )
7 6 exbidv 
 |-  ( -. y e. x -> ( E. z z e. x <-> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
8 4 7 bitrid 
 |-  ( -. y e. x -> ( x =/= (/) <-> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
9 8 pm5.74i 
 |-  ( ( -. y e. x -> x =/= (/) ) <-> ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
10 9 albii 
 |-  ( A. y ( -. y e. x -> x =/= (/) ) <-> A. y ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
11 2 3 10 3bitr2i 
 |-  ( x =/= (/) <-> A. y ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
12 df-ss 
 |-  ( x C_ U. x <-> A. y ( y e. x -> y e. U. x ) )
13 eluni 
 |-  ( y e. U. x <-> E. z ( y e. z /\ z e. x ) )
14 biimt 
 |-  ( y e. x -> ( y e. z <-> ( y e. x -> y e. z ) ) )
15 14 anbi1d 
 |-  ( y e. x -> ( ( y e. z /\ z e. x ) <-> ( ( y e. x -> y e. z ) /\ z e. x ) ) )
16 15 exbidv 
 |-  ( y e. x -> ( E. z ( y e. z /\ z e. x ) <-> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
17 13 16 bitrid 
 |-  ( y e. x -> ( y e. U. x <-> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
18 17 pm5.74i 
 |-  ( ( y e. x -> y e. U. x ) <-> ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
19 18 albii 
 |-  ( A. y ( y e. x -> y e. U. x ) <-> A. y ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
20 12 19 bitri 
 |-  ( x C_ U. x <-> A. y ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) )
21 11 20 anbi12ci 
 |-  ( ( x =/= (/) /\ x C_ U. x ) <-> ( A. y ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) /\ A. y ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) ) )
22 19.26 
 |-  ( A. y ( ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) /\ ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) ) <-> ( A. y ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) /\ A. y ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) ) )
23 pm4.83 
 |-  ( ( ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) /\ ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) ) <-> E. z ( ( y e. x -> y e. z ) /\ z e. x ) )
24 exnalimn 
 |-  ( E. z ( ( y e. x -> y e. z ) /\ z e. x ) <-> -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )
25 23 24 bitri 
 |-  ( ( ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) /\ ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) ) <-> -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )
26 25 albii 
 |-  ( A. y ( ( y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) /\ ( -. y e. x -> E. z ( ( y e. x -> y e. z ) /\ z e. x ) ) ) <-> A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )
27 21 22 26 3bitr2i 
 |-  ( ( x =/= (/) /\ x C_ U. x ) <-> A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )
28 27 exbii 
 |-  ( E. x ( x =/= (/) /\ x C_ U. x ) <-> E. x A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )
29 df-ex 
 |-  ( E. x A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) <-> -. A. x -. A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )
30 28 29 bitri 
 |-  ( E. x ( x =/= (/) /\ x C_ U. x ) <-> -. A. x -. A. y -. A. z ( ( y e. x -> y e. z ) -> -. z e. x ) )