Metamath Proof Explorer

Theorem mh-infprim3bi

Description: An axiom of infinity in primitive symbols not requiring ax-reg . This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines . It directly implies ax-inf , but deriving ax-inf2 requires ax-ext and ax-rep , see mh-inf3sn . (Contributed by Matthew House, 13-Apr-2026)

Ref Expression
Assertion mh-infprim3bi 
|- ( E. y ( x e. y /\ A. z e. y { z } e. y ) <-> -. A. y -. -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( z = x -> { z } = { x } )
2 1 eleq1d 
 |-  ( z = x -> ( { z } e. y <-> { x } e. y ) )
3 2 cbvralvw 
 |-  ( A. z e. y { z } e. y <-> A. x e. y { x } e. y )
4 dfclel 
 |-  ( { x } e. y <-> E. z ( z = { x } /\ z e. y ) )
5 dfcleq 
 |-  ( z = { x } <-> A. y ( y e. z <-> y e. { x } ) )
6 velsn 
 |-  ( y e. { x } <-> y = x )
7 6 bibi2i 
 |-  ( ( y e. z <-> y e. { x } ) <-> ( y e. z <-> y = x ) )
8 dfbi1 
 |-  ( ( y e. z <-> y = x ) <-> -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) )
9 7 8 bitri 
 |-  ( ( y e. z <-> y e. { x } ) <-> -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) )
10 9 albii 
 |-  ( A. y ( y e. z <-> y e. { x } ) <-> A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) )
11 5 10 bitri 
 |-  ( z = { x } <-> A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) )
12 11 anbi2ci 
 |-  ( ( z = { x } /\ z e. y ) <-> ( z e. y /\ A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
13 df-an 
 |-  ( ( z e. y /\ A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) <-> -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
14 12 13 bitri 
 |-  ( ( z = { x } /\ z e. y ) <-> -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
15 14 exbii 
 |-  ( E. z ( z = { x } /\ z e. y ) <-> E. z -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
16 df-ex 
 |-  ( E. z -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) <-> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
17 4 15 16 3bitri 
 |-  ( { x } e. y <-> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
18 17 ralbii 
 |-  ( A. x e. y { x } e. y <-> A. x e. y -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) )
19 df-ral 
 |-  ( A. x e. y -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) <-> A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) )
20 3 18 19 3bitri 
 |-  ( A. z e. y { z } e. y <-> A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) )
21 20 anbi2i 
 |-  ( ( x e. y /\ A. z e. y { z } e. y ) <-> ( x e. y /\ A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )
22 df-an 
 |-  ( ( x e. y /\ A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) <-> -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )
23 21 22 bitri 
 |-  ( ( x e. y /\ A. z e. y { z } e. y ) <-> -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )
24 23 exbii 
 |-  ( E. y ( x e. y /\ A. z e. y { z } e. y ) <-> E. y -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )
25 df-ex 
 |-  ( E. y -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) <-> -. A. y -. -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )
26 24 25 bitri 
 |-  ( E. y ( x e. y /\ A. z e. y { z } e. y ) <-> -. A. y -. -. ( x e. y -> -. A. x ( x e. y -> -. A. z -. -. ( z e. y -> -. A. y -. ( ( y e. z -> y = x ) -> -. ( y = x -> y e. z ) ) ) ) ) )