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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | weso | |
|
2 | 1 | 3ad2ant1 | |
3 | simp1 | |
|
4 | simp2 | |
|
5 | ssidd | |
|
6 | simp3 | |
|
7 | tz6.26 | |
|
8 | 3 4 5 6 7 | syl22anc | |
9 | vex | |
|
10 | 9 | elpred | |
11 | 10 | elv | |
12 | 11 | notbii | |
13 | imnan | |
|
14 | 12 13 | bitr4i | |
15 | pm2.27 | |
|
16 | 15 | ad2antll | |
17 | breq1 | |
|
18 | 17 | rspcev | |
19 | 18 | ex | |
20 | 19 | ad2antrl | |
21 | 16 20 | jctird | |
22 | 14 21 | biimtrid | |
23 | 22 | expr | |
24 | 23 | com23 | |
25 | 24 | alimdv | |
26 | eq0 | |
|
27 | r19.26 | |
|
28 | df-ral | |
|
29 | 27 28 | bitr3i | |
30 | 25 26 29 | 3imtr4g | |
31 | 30 | reximdva | |
32 | 8 31 | mpd | |
33 | 2 32 | infcl | |