Metamath Proof Explorer

Theorem wsuclem

Description: Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

Ref Expression
Hypotheses wsuclem.1 
|- ( ph -> R We A )
wsuclem.2 
|- ( ph -> R Se A )
wsuclem.3 
|- ( ph -> X e. V )
wsuclem.4 
|- ( ph -> E. w e. A X R w )
Assertion wsuclem 
|- ( ph -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) )

Proof

Step Hyp Ref Expression
1 wsuclem.1 
 |-  ( ph -> R We A )
2 wsuclem.2 
 |-  ( ph -> R Se A )
3 wsuclem.3 
 |-  ( ph -> X e. V )
4 wsuclem.4 
 |-  ( ph -> E. w e. A X R w )
5 predss 
 |-  Pred ( `' R , A , X ) C_ A
6 5 a1i 
 |-  ( ph -> Pred ( `' R , A , X ) C_ A )
7 dfpred3g 
 |-  ( X e. V -> Pred ( `' R , A , X ) = { w e. A | w `' R X } )
8 3 7 syl 
 |-  ( ph -> Pred ( `' R , A , X ) = { w e. A | w `' R X } )
9 3 elexd 
 |-  ( ph -> X e. _V )
10 rabn0 
 |-  ( { w e. A | w `' R X } =/= (/) <-> E. w e. A w `' R X )
11 brcnvg 
 |-  ( ( w e. A /\ X e. _V ) -> ( w `' R X <-> X R w ) )
12 11 ancoms 
 |-  ( ( X e. _V /\ w e. A ) -> ( w `' R X <-> X R w ) )
13 12 rexbidva 
 |-  ( X e. _V -> ( E. w e. A w `' R X <-> E. w e. A X R w ) )
14 10 13 bitrid 
 |-  ( X e. _V -> ( { w e. A | w `' R X } =/= (/) <-> E. w e. A X R w ) )
15 14 biimpar 
 |-  ( ( X e. _V /\ E. w e. A X R w ) -> { w e. A | w `' R X } =/= (/) )
16 9 4 15 syl2anc 
 |-  ( ph -> { w e. A | w `' R X } =/= (/) )
17 8 16 eqnetrd 
 |-  ( ph -> Pred ( `' R , A , X ) =/= (/) )
18 tz6.26 
 |-  ( ( ( R We A /\ R Se A ) /\ ( Pred ( `' R , A , X ) C_ A /\ Pred ( `' R , A , X ) =/= (/) ) ) -> E. x e. Pred ( `' R , A , X ) Pred ( R , Pred ( `' R , A , X ) , x ) = (/) )
19 1 2 6 17 18 syl22anc 
 |-  ( ph -> E. x e. Pred ( `' R , A , X ) Pred ( R , Pred ( `' R , A , X ) , x ) = (/) )
20 dfpred3g 
 |-  ( X e. V -> Pred ( `' R , A , X ) = { y e. A | y `' R X } )
21 3 20 syl 
 |-  ( ph -> Pred ( `' R , A , X ) = { y e. A | y `' R X } )
22 21 rexeqdv 
 |-  ( ph -> ( E. x e. Pred ( `' R , A , X ) Pred ( R , Pred ( `' R , A , X ) , x ) = (/) <-> E. x e. { y e. A | y `' R X } Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) )
23 breq1 
 |-  ( y = x -> ( y `' R X <-> x `' R X ) )
24 23 rexrab 
 |-  ( E. x e. { y e. A | y `' R X } Pred ( R , Pred ( `' R , A , X ) , x ) = (/) <-> E. x e. A ( x `' R X /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) )
25 noel 
 |-  -. y e. (/)
26 simp2r 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> Pred ( R , Pred ( `' R , A , X ) , x ) = (/) )
27 26 eleq2d 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> ( y e. Pred ( R , Pred ( `' R , A , X ) , x ) <-> y e. (/) ) )
28 25 27 mtbiri 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> -. y e. Pred ( R , Pred ( `' R , A , X ) , x ) )
29 vex 
 |-  x e. _V
30 29 a1i 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> x e. _V )
31 simp3 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> y e. Pred ( `' R , A , X ) )
32 elpredg 
 |-  ( ( x e. _V /\ y e. Pred ( `' R , A , X ) ) -> ( y e. Pred ( R , Pred ( `' R , A , X ) , x ) <-> y R x ) )
33 30 31 32 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> ( y e. Pred ( R , Pred ( `' R , A , X ) , x ) <-> y R x ) )
34 28 33 mtbid 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) /\ y e. Pred ( `' R , A , X ) ) -> -. y R x )
35 34 3expa 
 |-  ( ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) ) /\ y e. Pred ( `' R , A , X ) ) -> -. y R x )
36 35 ralrimiva 
 |-  ( ( ph /\ ( x e. A /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) ) -> A. y e. Pred ( `' R , A , X ) -. y R x )
37 36 expr 
 |-  ( ( ph /\ x e. A ) -> ( Pred ( R , Pred ( `' R , A , X ) , x ) = (/) -> A. y e. Pred ( `' R , A , X ) -. y R x ) )
38 simp1rl 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> x e. A )
39 simp1rr 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> x `' R X )
40 3 adantr 
 |-  ( ( ph /\ ( x e. A /\ x `' R X ) ) -> X e. V )
41 40 3ad2ant1 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> X e. V )
42 29 elpred 
 |-  ( X e. V -> ( x e. Pred ( `' R , A , X ) <-> ( x e. A /\ x `' R X ) ) )
43 41 42 syl 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> ( x e. Pred ( `' R , A , X ) <-> ( x e. A /\ x `' R X ) ) )
44 38 39 43 mpbir2and 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> x e. Pred ( `' R , A , X ) )
45 simp3 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> x R y )
46 breq1 
 |-  ( z = x -> ( z R y <-> x R y ) )
47 46 rspcev 
 |-  ( ( x e. Pred ( `' R , A , X ) /\ x R y ) -> E. z e. Pred ( `' R , A , X ) z R y )
48 44 45 47 syl2anc 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A /\ x R y ) -> E. z e. Pred ( `' R , A , X ) z R y )
49 48 3expia 
 |-  ( ( ( ph /\ ( x e. A /\ x `' R X ) ) /\ y e. A ) -> ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) )
50 49 ralrimiva 
 |-  ( ( ph /\ ( x e. A /\ x `' R X ) ) -> A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) )
51 50 expr 
 |-  ( ( ph /\ x e. A ) -> ( x `' R X -> A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) )
52 37 51 anim12d 
 |-  ( ( ph /\ x e. A ) -> ( ( Pred ( R , Pred ( `' R , A , X ) , x ) = (/) /\ x `' R X ) -> ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) ) )
53 52 ancomsd 
 |-  ( ( ph /\ x e. A ) -> ( ( x `' R X /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) -> ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) ) )
54 53 reximdva 
 |-  ( ph -> ( E. x e. A ( x `' R X /\ Pred ( R , Pred ( `' R , A , X ) , x ) = (/) ) -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) ) )
55 24 54 biimtrid 
 |-  ( ph -> ( E. x e. { y e. A | y `' R X } Pred ( R , Pred ( `' R , A , X ) , x ) = (/) -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) ) )
56 22 55 sylbid 
 |-  ( ph -> ( E. x e. Pred ( `' R , A , X ) Pred ( R , Pred ( `' R , A , X ) , x ) = (/) -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) ) )
57 19 56 mpd 
 |-  ( ph -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) )