Metamath Proof Explorer

Theorem omssaxinf2

Description: A class that contains all ordinals up to and including _om models the Axiom of Infinity ax-inf2 . The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf . (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion omssaxinf2 
|- ( ( _om C_ M /\ _om e. M ) -> E. x e. M ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 ssel 
 |-  ( _om C_ M -> ( (/) e. _om -> (/) e. M ) )
3 1 2 mpi 
 |-  ( _om C_ M -> (/) e. M )
4 noel 
 |-  -. z e. (/)
5 4 rgenw 
 |-  A. z e. M -. z e. (/)
6 eleq1 
 |-  ( y = (/) -> ( y e. _om <-> (/) e. _om ) )
7 eleq2 
 |-  ( y = (/) -> ( z e. y <-> z e. (/) ) )
8 7 notbid 
 |-  ( y = (/) -> ( -. z e. y <-> -. z e. (/) ) )
9 8 ralbidv 
 |-  ( y = (/) -> ( A. z e. M -. z e. y <-> A. z e. M -. z e. (/) ) )
10 6 9 anbi12d 
 |-  ( y = (/) -> ( ( y e. _om /\ A. z e. M -. z e. y ) <-> ( (/) e. _om /\ A. z e. M -. z e. (/) ) ) )
11 10 rspcev 
 |-  ( ( (/) e. M /\ ( (/) e. _om /\ A. z e. M -. z e. (/) ) ) -> E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) )
12 1 5 11 mpanr12 
 |-  ( (/) e. M -> E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) )
13 3 12 syl 
 |-  ( _om C_ M -> E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) )
14 ssel 
 |-  ( _om C_ M -> ( suc y e. _om -> suc y e. M ) )
15 peano2 
 |-  ( y e. _om -> suc y e. _om )
16 14 15 impel 
 |-  ( ( _om C_ M /\ y e. _om ) -> suc y e. M )
17 15 adantl 
 |-  ( ( _om C_ M /\ y e. _om ) -> suc y e. _om )
18 vex 
 |-  w e. _V
19 18 elsuc 
 |-  ( w e. suc y <-> ( w e. y \/ w = y ) )
20 19 rgenw 
 |-  A. w e. M ( w e. suc y <-> ( w e. y \/ w = y ) )
21 eleq1 
 |-  ( z = suc y -> ( z e. _om <-> suc y e. _om ) )
22 eleq2 
 |-  ( z = suc y -> ( w e. z <-> w e. suc y ) )
23 22 bibi1d 
 |-  ( z = suc y -> ( ( w e. z <-> ( w e. y \/ w = y ) ) <-> ( w e. suc y <-> ( w e. y \/ w = y ) ) ) )
24 23 ralbidv 
 |-  ( z = suc y -> ( A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) <-> A. w e. M ( w e. suc y <-> ( w e. y \/ w = y ) ) ) )
25 21 24 anbi12d 
 |-  ( z = suc y -> ( ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) <-> ( suc y e. _om /\ A. w e. M ( w e. suc y <-> ( w e. y \/ w = y ) ) ) ) )
26 25 rspcev 
 |-  ( ( suc y e. M /\ ( suc y e. _om /\ A. w e. M ( w e. suc y <-> ( w e. y \/ w = y ) ) ) ) -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) )
27 20 26 mpanr2 
 |-  ( ( suc y e. M /\ suc y e. _om ) -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) )
28 16 17 27 syl2anc 
 |-  ( ( _om C_ M /\ y e. _om ) -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) )
29 28 ex 
 |-  ( _om C_ M -> ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
30 29 ralrimivw 
 |-  ( _om C_ M -> A. y e. M ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
31 eleq2 
 |-  ( x = _om -> ( y e. x <-> y e. _om ) )
32 31 anbi1d 
 |-  ( x = _om -> ( ( y e. x /\ A. z e. M -. z e. y ) <-> ( y e. _om /\ A. z e. M -. z e. y ) ) )
33 32 rexbidv 
 |-  ( x = _om -> ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) <-> E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) ) )
34 eleq2 
 |-  ( x = _om -> ( z e. x <-> z e. _om ) )
35 34 anbi1d 
 |-  ( x = _om -> ( ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) <-> ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
36 35 rexbidv 
 |-  ( x = _om -> ( E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) <-> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
37 31 36 imbi12d 
 |-  ( x = _om -> ( ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) <-> ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )
38 37 ralbidv 
 |-  ( x = _om -> ( A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) <-> A. y e. M ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )
39 33 38 anbi12d 
 |-  ( x = _om -> ( ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) <-> ( E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) ) )
40 39 rspcev 
 |-  ( ( _om e. M /\ ( E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) ) -> E. x e. M ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )
41 40 expcom 
 |-  ( ( E. y e. M ( y e. _om /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. _om -> E. z e. M ( z e. _om /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) -> ( _om e. M -> E. x e. M ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) ) )
42 13 30 41 syl2anc 
 |-  ( _om C_ M -> ( _om e. M -> E. x e. M ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) ) )
43 42 imp 
 |-  ( ( _om C_ M /\ _om e. M ) -> E. x e. M ( E. y e. M ( y e. x /\ A. z e. M -. z e. y ) /\ A. y e. M ( y e. x -> E. z e. M ( z e. x /\ A. w e. M ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )