Metamath Proof Explorer

Theorem wzel

Description: The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018) (Revised by AV, 10-Oct-2021)

Ref Expression
Assertion wzel 
|- ( ( R We A /\ R Se A /\ A =/= (/) ) -> inf ( A , A , R ) e. A )

Proof

Step Hyp Ref Expression
1 weso 
 |-  ( R We A -> R Or A )
2 1 3ad2ant1 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> R Or A )
3 simp1 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> R We A )
4 simp2 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> R Se A )
5 ssidd 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> A C_ A )
6 simp3 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> A =/= (/) )
7 tz6.26 
 |-  ( ( ( R We A /\ R Se A ) /\ ( A C_ A /\ A =/= (/) ) ) -> E. x e. A Pred ( R , A , x ) = (/) )
8 3 4 5 6 7 syl22anc 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> E. x e. A Pred ( R , A , x ) = (/) )
9 vex 
 |-  y e. _V
10 9 elpred 
 |-  ( x e. _V -> ( y e. Pred ( R , A , x ) <-> ( y e. A /\ y R x ) ) )
11 10 elv 
 |-  ( y e. Pred ( R , A , x ) <-> ( y e. A /\ y R x ) )
12 11 notbii 
 |-  ( -. y e. Pred ( R , A , x ) <-> -. ( y e. A /\ y R x ) )
13 imnan 
 |-  ( ( y e. A -> -. y R x ) <-> -. ( y e. A /\ y R x ) )
14 12 13 bitr4i 
 |-  ( -. y e. Pred ( R , A , x ) <-> ( y e. A -> -. y R x ) )
15 pm2.27 
 |-  ( y e. A -> ( ( y e. A -> -. y R x ) -> -. y R x ) )
16 15 ad2antll 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ ( x e. A /\ y e. A ) ) -> ( ( y e. A -> -. y R x ) -> -. y R x ) )
17 breq1 
 |-  ( z = x -> ( z R y <-> x R y ) )
18 17 rspcev 
 |-  ( ( x e. A /\ x R y ) -> E. z e. A z R y )
19 18 ex 
 |-  ( x e. A -> ( x R y -> E. z e. A z R y ) )
20 19 ad2antrl 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ ( x e. A /\ y e. A ) ) -> ( x R y -> E. z e. A z R y ) )
21 16 20 jctird 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ ( x e. A /\ y e. A ) ) -> ( ( y e. A -> -. y R x ) -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) )
22 14 21 syl5bi 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ ( x e. A /\ y e. A ) ) -> ( -. y e. Pred ( R , A , x ) -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) )
23 22 expr 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ x e. A ) -> ( y e. A -> ( -. y e. Pred ( R , A , x ) -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) ) )
24 23 com23 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ x e. A ) -> ( -. y e. Pred ( R , A , x ) -> ( y e. A -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) ) )
25 24 alimdv 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ x e. A ) -> ( A. y -. y e. Pred ( R , A , x ) -> A. y ( y e. A -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) ) )
26 eq0 
 |-  ( Pred ( R , A , x ) = (/) <-> A. y -. y e. Pred ( R , A , x ) )
27 r19.26 
 |-  ( A. y e. A ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) <-> ( A. y e. A -. y R x /\ A. y e. A ( x R y -> E. z e. A z R y ) ) )
28 df-ral 
 |-  ( A. y e. A ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) <-> A. y ( y e. A -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) )
29 27 28 bitr3i 
 |-  ( ( A. y e. A -. y R x /\ A. y e. A ( x R y -> E. z e. A z R y ) ) <-> A. y ( y e. A -> ( -. y R x /\ ( x R y -> E. z e. A z R y ) ) ) )
30 25 26 29 3imtr4g 
 |-  ( ( ( R We A /\ R Se A /\ A =/= (/) ) /\ x e. A ) -> ( Pred ( R , A , x ) = (/) -> ( A. y e. A -. y R x /\ A. y e. A ( x R y -> E. z e. A z R y ) ) ) )
31 30 reximdva 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> ( E. x e. A Pred ( R , A , x ) = (/) -> E. x e. A ( A. y e. A -. y R x /\ A. y e. A ( x R y -> E. z e. A z R y ) ) ) )
32 8 31 mpd 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> E. x e. A ( A. y e. A -. y R x /\ A. y e. A ( x R y -> E. z e. A z R y ) ) )
33 2 32 infcl 
 |-  ( ( R We A /\ R Se A /\ A =/= (/) ) -> inf ( A , A , R ) e. A )