Metamath Proof Explorer


Theorem satfdmlem

Description: Lemma for satfdm . (Contributed by AV, 12-Oct-2023)

Ref Expression
Assertion satfdmlem MVEWYωdomMSatEY=domNSatFYuMSatEYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta

Proof

Step Hyp Ref Expression
1 satfrel MVEWYωRelMSatEY
2 1 adantr MVEWYωdomMSatEY=domNSatFYRelMSatEY
3 1stdm RelMSatEYuMSatEY1studomMSatEY
4 2 3 sylan MVEWYωdomMSatEY=domNSatFYuMSatEY1studomMSatEY
5 eleq2 domMSatEY=domNSatFY1studomMSatEY1studomNSatFY
6 5 adantl MVEWYωdomMSatEY=domNSatFY1studomMSatEY1studomNSatFY
7 6 adantr MVEWYωdomMSatEY=domNSatFYuMSatEY1studomMSatEY1studomNSatFY
8 fvex 1stuV
9 eldm2g 1stuV1studomNSatFYs1stusNSatFY
10 8 9 ax-mp 1studomNSatFYs1stusNSatFY
11 simpr MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFY1stusNSatFY
12 2 ad4antr MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEYRelMSatEY
13 1stdm RelMSatEYvMSatEY1stvdomMSatEY
14 12 13 sylancom MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvdomMSatEY
15 eleq2 domMSatEY=domNSatFY1stvdomMSatEY1stvdomNSatFY
16 15 ad5antlr MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvdomMSatEY1stvdomNSatFY
17 fvex 1stvV
18 eldm2g 1stvV1stvdomNSatFYr1stvrNSatFY
19 17 18 ax-mp 1stvdomNSatFYr1stvrNSatFY
20 simpr MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFY1stvrNSatFY
21 vex sV
22 8 21 op1std a=1stus1sta=1stu
23 22 eqcomd a=1stus1stu=1sta
24 23 ad3antlr MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFY1stu=1sta
25 vex rV
26 17 25 op1std b=1stvr1stb=1stv
27 26 eqcomd b=1stvr1stv=1stb
28 24 27 oveqan12d MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFYb=1stvr1stu𝑔1stv=1sta𝑔1stb
29 28 eqeq2d MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFYb=1stvrx=1stu𝑔1stvx=1sta𝑔1stb
30 29 biimpd MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFYb=1stvrx=1stu𝑔1stvx=1sta𝑔1stb
31 20 30 rspcimedv MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
32 31 ex MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvrNSatFYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
33 32 exlimdv MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEYr1stvrNSatFYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
34 19 33 syl5bi MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvdomNSatFYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
35 16 34 sylbid MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEY1stvdomMSatEYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
36 14 35 mpd MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
37 36 rexlimdva MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEYx=1stu𝑔1stvbNSatFYx=1sta𝑔1stb
38 eqidd a=1stusi=i
39 38 23 goaleq12d a=1stus𝑔i1stu=𝑔i1sta
40 39 eqeq2d a=1stusx=𝑔i1stux=𝑔i1sta
41 40 biimpd a=1stusx=𝑔i1stux=𝑔i1sta
42 41 adantl MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusx=𝑔i1stux=𝑔i1sta
43 42 reximdv MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusiωx=𝑔i1stuiωx=𝑔i1sta
44 37 43 orim12d MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYa=1stusvMSatEYx=1stu𝑔1stviωx=𝑔i1stubNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
45 11 44 rspcimedv MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
46 45 ex MVEWYωdomMSatEY=domNSatFYuMSatEY1stusNSatFYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
47 46 exlimdv MVEWYωdomMSatEY=domNSatFYuMSatEYs1stusNSatFYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
48 10 47 syl5bi MVEWYωdomMSatEY=domNSatFYuMSatEY1studomNSatFYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
49 7 48 sylbid MVEWYωdomMSatEY=domNSatFYuMSatEY1studomMSatEYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
50 4 49 mpd MVEWYωdomMSatEY=domNSatFYuMSatEYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta
51 50 rexlimdva MVEWYωdomMSatEY=domNSatFYuMSatEYvMSatEYx=1stu𝑔1stviωx=𝑔i1stuaNSatFYbNSatFYx=1sta𝑔1stbiωx=𝑔i1sta