Description: Lemma for satfdm . (Contributed by AV, 12-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | satfdmlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | satfrel | |
|
2 | 1 | adantr | |
3 | 1stdm | |
|
4 | 2 3 | sylan | |
5 | eleq2 | |
|
6 | 5 | adantl | |
7 | 6 | adantr | |
8 | fvex | |
|
9 | eldm2g | |
|
10 | 8 9 | ax-mp | |
11 | simpr | |
|
12 | 2 | ad4antr | |
13 | 1stdm | |
|
14 | 12 13 | sylancom | |
15 | eleq2 | |
|
16 | 15 | ad5antlr | |
17 | fvex | |
|
18 | eldm2g | |
|
19 | 17 18 | ax-mp | |
20 | simpr | |
|
21 | vex | |
|
22 | 8 21 | op1std | |
23 | 22 | eqcomd | |
24 | 23 | ad3antlr | |
25 | vex | |
|
26 | 17 25 | op1std | |
27 | 26 | eqcomd | |
28 | 24 27 | oveqan12d | |
29 | 28 | eqeq2d | |
30 | 29 | biimpd | |
31 | 20 30 | rspcimedv | |
32 | 31 | ex | |
33 | 32 | exlimdv | |
34 | 19 33 | syl5bi | |
35 | 16 34 | sylbid | |
36 | 14 35 | mpd | |
37 | 36 | rexlimdva | |
38 | eqidd | |
|
39 | 38 23 | goaleq12d | |
40 | 39 | eqeq2d | |
41 | 40 | biimpd | |
42 | 41 | adantl | |
43 | 42 | reximdv | |
44 | 37 43 | orim12d | |
45 | 11 44 | rspcimedv | |
46 | 45 | ex | |
47 | 46 | exlimdv | |
48 | 10 47 | syl5bi | |
49 | 7 48 | sylbid | |
50 | 4 49 | mpd | |
51 | 50 | rexlimdva | |