Metamath Proof Explorer

Theorem mh-infprim2bi

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

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

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( y = z -> { y } = { z } )
2 1 eleq1d 
 |-  ( y = z -> ( { y } e. x <-> { z } e. x ) )
3 2 cbvralvw 
 |-  ( A. y e. x { y } e. x <-> A. z e. x { z } e. x )
4 df-ral 
 |-  ( A. z e. x { z } e. x <-> A. z ( z e. x -> { z } e. x ) )
5 3 4 bitri 
 |-  ( A. y e. x { y } e. x <-> A. z ( z e. x -> { z } e. x ) )
6 5 anbi2i 
 |-  ( ( (/) e. x /\ A. y e. x { y } e. x ) <-> ( (/) e. x /\ A. z ( z e. x -> { z } e. x ) ) )
7 pwin 
 |-  ~P ( { z } i^i x ) = ( ~P { z } i^i ~P x )
8 7 raleqi 
 |-  ( A. y e. ~P ( { z } i^i x ) y e. x <-> A. y e. ( ~P { z } i^i ~P x ) y e. x )
9 ralin 
 |-  ( A. y e. ( ~P { z } i^i ~P x ) y e. x <-> A. y e. ~P { z } ( y e. ~P x -> y e. x ) )
10 pwsn 
 |-  ~P { z } = { (/) , { z } }
11 10 raleqi 
 |-  ( A. y e. ~P { z } ( y e. ~P x -> y e. x ) <-> A. y e. { (/) , { z } } ( y e. ~P x -> y e. x ) )
12 8 9 11 3bitrri 
 |-  ( A. y e. { (/) , { z } } ( y e. ~P x -> y e. x ) <-> A. y e. ~P ( { z } i^i x ) y e. x )
13 0ex 
 |-  (/) e. _V
14 vsnex 
 |-  { z } e. _V
15 eleq1 
 |-  ( y = (/) -> ( y e. ~P x <-> (/) e. ~P x ) )
16 eleq1 
 |-  ( y = (/) -> ( y e. x <-> (/) e. x ) )
17 15 16 imbi12d 
 |-  ( y = (/) -> ( ( y e. ~P x -> y e. x ) <-> ( (/) e. ~P x -> (/) e. x ) ) )
18 0elpw 
 |-  (/) e. ~P x
19 18 a1bi 
 |-  ( (/) e. x <-> ( (/) e. ~P x -> (/) e. x ) )
20 17 19 bitr4di 
 |-  ( y = (/) -> ( ( y e. ~P x -> y e. x ) <-> (/) e. x ) )
21 eleq1 
 |-  ( y = { z } -> ( y e. ~P x <-> { z } e. ~P x ) )
22 vex 
 |-  z e. _V
23 22 snelpw 
 |-  ( z e. x <-> { z } e. ~P x )
24 21 23 bitr4di 
 |-  ( y = { z } -> ( y e. ~P x <-> z e. x ) )
25 eleq1 
 |-  ( y = { z } -> ( y e. x <-> { z } e. x ) )
26 24 25 imbi12d 
 |-  ( y = { z } -> ( ( y e. ~P x -> y e. x ) <-> ( z e. x -> { z } e. x ) ) )
27 13 14 20 26 ralpr 
 |-  ( A. y e. { (/) , { z } } ( y e. ~P x -> y e. x ) <-> ( (/) e. x /\ ( z e. x -> { z } e. x ) ) )
28 df-ral 
 |-  ( A. y e. ~P ( { z } i^i x ) y e. x <-> A. y ( y e. ~P ( { z } i^i x ) -> y e. x ) )
29 12 27 28 3bitr3i 
 |-  ( ( (/) e. x /\ ( z e. x -> { z } e. x ) ) <-> A. y ( y e. ~P ( { z } i^i x ) -> y e. x ) )
30 29 albii 
 |-  ( A. z ( (/) e. x /\ ( z e. x -> { z } e. x ) ) <-> A. z A. y ( y e. ~P ( { z } i^i x ) -> y e. x ) )
31 19.28v 
 |-  ( A. z ( (/) e. x /\ ( z e. x -> { z } e. x ) ) <-> ( (/) e. x /\ A. z ( z e. x -> { z } e. x ) ) )
32 sneq 
 |-  ( z = w -> { z } = { w } )
33 32 ineq1d 
 |-  ( z = w -> ( { z } i^i x ) = ( { w } i^i x ) )
34 33 pweqd 
 |-  ( z = w -> ~P ( { z } i^i x ) = ~P ( { w } i^i x ) )
35 34 eleq2d 
 |-  ( z = w -> ( y e. ~P ( { z } i^i x ) <-> y e. ~P ( { w } i^i x ) ) )
36 35 imbi1d 
 |-  ( z = w -> ( ( y e. ~P ( { z } i^i x ) -> y e. x ) <-> ( y e. ~P ( { w } i^i x ) -> y e. x ) ) )
37 eleq1w 
 |-  ( y = w -> ( y e. ~P ( { z } i^i x ) <-> w e. ~P ( { z } i^i x ) ) )
38 elequ1 
 |-  ( y = w -> ( y e. x <-> w e. x ) )
39 37 38 imbi12d 
 |-  ( y = w -> ( ( y e. ~P ( { z } i^i x ) -> y e. x ) <-> ( w e. ~P ( { z } i^i x ) -> w e. x ) ) )
40 36 39 alcomw 
 |-  ( A. z A. y ( y e. ~P ( { z } i^i x ) -> y e. x ) <-> A. y A. z ( y e. ~P ( { z } i^i x ) -> y e. x ) )
41 30 31 40 3bitr3i 
 |-  ( ( (/) e. x /\ A. z ( z e. x -> { z } e. x ) ) <-> A. y A. z ( y e. ~P ( { z } i^i x ) -> y e. x ) )
42 velpw 
 |-  ( y e. ~P ( { z } i^i x ) <-> y C_ ( { z } i^i x ) )
43 df-ss 
 |-  ( y C_ ( { z } i^i x ) <-> A. w ( w e. y -> w e. ( { z } i^i x ) ) )
44 elin 
 |-  ( w e. ( { z } i^i x ) <-> ( w e. { z } /\ w e. x ) )
45 velsn 
 |-  ( w e. { z } <-> w = z )
46 45 anbi2ci 
 |-  ( ( w e. { z } /\ w e. x ) <-> ( w e. x /\ w = z ) )
47 df-an 
 |-  ( ( w e. x /\ w = z ) <-> -. ( w e. x -> -. w = z ) )
48 44 46 47 3bitri 
 |-  ( w e. ( { z } i^i x ) <-> -. ( w e. x -> -. w = z ) )
49 48 imbi2i 
 |-  ( ( w e. y -> w e. ( { z } i^i x ) ) <-> ( w e. y -> -. ( w e. x -> -. w = z ) ) )
50 49 albii 
 |-  ( A. w ( w e. y -> w e. ( { z } i^i x ) ) <-> A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) )
51 42 43 50 3bitri 
 |-  ( y e. ~P ( { z } i^i x ) <-> A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) )
52 51 imbi1i 
 |-  ( ( y e. ~P ( { z } i^i x ) -> y e. x ) <-> ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) )
53 52 2albii 
 |-  ( A. y A. z ( y e. ~P ( { z } i^i x ) -> y e. x ) <-> A. y A. z ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) )
54 6 41 53 3bitri 
 |-  ( ( (/) e. x /\ A. y e. x { y } e. x ) <-> A. y A. z ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) )
55 54 exbii 
 |-  ( E. x ( (/) e. x /\ A. y e. x { y } e. x ) <-> E. x A. y A. z ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) )
56 df-ex 
 |-  ( E. x A. y A. z ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) <-> -. A. x -. A. y A. z ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) )
57 55 56 bitri 
 |-  ( E. x ( (/) e. x /\ A. y e. x { y } e. x ) <-> -. A. x -. A. y A. z ( A. w ( w e. y -> -. ( w e. x -> -. w = z ) ) -> y e. x ) )