Metamath Proof Explorer

Theorem sswfaxreg

Description: A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg . Lemma II.2.4(2) of Kunen2 p. 111. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion sswfaxreg 
|- ( M C_ U. ( R1 " On ) -> A. x e. M ( E. y e. M y e. x -> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) ) )

Proof

Step Hyp Ref Expression
1 inn0 
 |-  ( ( M i^i x ) =/= (/) <-> E. y e. M y e. x )
2 ssinss1 
 |-  ( M C_ U. ( R1 " On ) -> ( M i^i x ) C_ U. ( R1 " On ) )
3 vex 
 |-  x e. _V
4 3 inex2 
 |-  ( M i^i x ) e. _V
5 wffr 
 |-  _E Fr U. ( R1 " On )
6 fri 
 |-  ( ( ( ( M i^i x ) e. _V /\ _E Fr U. ( R1 " On ) ) /\ ( ( M i^i x ) C_ U. ( R1 " On ) /\ ( M i^i x ) =/= (/) ) ) -> E. y e. ( M i^i x ) A. z e. ( M i^i x ) -. z _E y )
7 4 5 6 mpanl12 
 |-  ( ( ( M i^i x ) C_ U. ( R1 " On ) /\ ( M i^i x ) =/= (/) ) -> E. y e. ( M i^i x ) A. z e. ( M i^i x ) -. z _E y )
8 2 7 sylan 
 |-  ( ( M C_ U. ( R1 " On ) /\ ( M i^i x ) =/= (/) ) -> E. y e. ( M i^i x ) A. z e. ( M i^i x ) -. z _E y )
9 ralin 
 |-  ( A. z e. ( M i^i x ) -. z _E y <-> A. z e. M ( z e. x -> -. z _E y ) )
10 con2b 
 |-  ( ( z e. x -> -. z _E y ) <-> ( z _E y -> -. z e. x ) )
11 epel 
 |-  ( z _E y <-> z e. y )
12 11 imbi1i 
 |-  ( ( z _E y -> -. z e. x ) <-> ( z e. y -> -. z e. x ) )
13 10 12 bitri 
 |-  ( ( z e. x -> -. z _E y ) <-> ( z e. y -> -. z e. x ) )
14 13 ralbii 
 |-  ( A. z e. M ( z e. x -> -. z _E y ) <-> A. z e. M ( z e. y -> -. z e. x ) )
15 9 14 bitri 
 |-  ( A. z e. ( M i^i x ) -. z _E y <-> A. z e. M ( z e. y -> -. z e. x ) )
16 15 rexbii 
 |-  ( E. y e. ( M i^i x ) A. z e. ( M i^i x ) -. z _E y <-> E. y e. ( M i^i x ) A. z e. M ( z e. y -> -. z e. x ) )
17 rexin 
 |-  ( E. y e. ( M i^i x ) A. z e. M ( z e. y -> -. z e. x ) <-> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) )
18 16 17 bitri 
 |-  ( E. y e. ( M i^i x ) A. z e. ( M i^i x ) -. z _E y <-> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) )
19 8 18 sylib 
 |-  ( ( M C_ U. ( R1 " On ) /\ ( M i^i x ) =/= (/) ) -> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) )
20 1 19 sylan2br 
 |-  ( ( M C_ U. ( R1 " On ) /\ E. y e. M y e. x ) -> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) )
21 20 ex 
 |-  ( M C_ U. ( R1 " On ) -> ( E. y e. M y e. x -> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) ) )
22 21 ralrimivw 
 |-  ( M C_ U. ( R1 " On ) -> A. x e. M ( E. y e. M y e. x -> E. y e. M ( y e. x /\ A. z e. M ( z e. y -> -. z e. x ) ) ) )