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 RWeARSeAAsupAARA

Proof

Step Hyp Ref Expression
1 weso RWeAROrA
2 1 3ad2ant1 RWeARSeAAROrA
3 simp1 RWeARSeAARWeA
4 simp2 RWeARSeAARSeA
5 ssidd RWeARSeAAAA
6 simp3 RWeARSeAAA
7 tz6.26 RWeARSeAAAAxAPredRAx=
8 3 4 5 6 7 syl22anc RWeARSeAAxAPredRAx=
9 vex yV
10 9 elpred xVyPredRAxyAyRx
11 10 elv yPredRAxyAyRx
12 11 notbii ¬yPredRAx¬yAyRx
13 imnan yA¬yRx¬yAyRx
14 12 13 bitr4i ¬yPredRAxyA¬yRx
15 pm2.27 yAyA¬yRx¬yRx
16 15 ad2antll RWeARSeAAxAyAyA¬yRx¬yRx
17 breq1 z=xzRyxRy
18 17 rspcev xAxRyzAzRy
19 18 ex xAxRyzAzRy
20 19 ad2antrl RWeARSeAAxAyAxRyzAzRy
21 16 20 jctird RWeARSeAAxAyAyA¬yRx¬yRxxRyzAzRy
22 14 21 biimtrid RWeARSeAAxAyA¬yPredRAx¬yRxxRyzAzRy
23 22 expr RWeARSeAAxAyA¬yPredRAx¬yRxxRyzAzRy
24 23 com23 RWeARSeAAxA¬yPredRAxyA¬yRxxRyzAzRy
25 24 alimdv RWeARSeAAxAy¬yPredRAxyyA¬yRxxRyzAzRy
26 eq0 PredRAx=y¬yPredRAx
27 r19.26 yA¬yRxxRyzAzRyyA¬yRxyAxRyzAzRy
28 df-ral yA¬yRxxRyzAzRyyyA¬yRxxRyzAzRy
29 27 28 bitr3i yA¬yRxyAxRyzAzRyyyA¬yRxxRyzAzRy
30 25 26 29 3imtr4g RWeARSeAAxAPredRAx=yA¬yRxyAxRyzAzRy
31 30 reximdva RWeARSeAAxAPredRAx=xAyA¬yRxyAxRyzAzRy
32 8 31 mpd RWeARSeAAxAyA¬yRxyAxRyzAzRy
33 2 32 infcl RWeARSeAAsupAARA