Metamath Proof Explorer


Theorem satfdmlem

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

Ref Expression
Assertion satfdmlem M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a

Proof

Step Hyp Ref Expression
1 satfrel M V E W Y ω Rel M Sat E Y
2 1 adantr M V E W Y ω dom M Sat E Y = dom N Sat F Y Rel M Sat E Y
3 1stdm Rel M Sat E Y u M Sat E Y 1 st u dom M Sat E Y
4 2 3 sylan M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u dom M Sat E Y
5 eleq2 dom M Sat E Y = dom N Sat F Y 1 st u dom M Sat E Y 1 st u dom N Sat F Y
6 5 adantl M V E W Y ω dom M Sat E Y = dom N Sat F Y 1 st u dom M Sat E Y 1 st u dom N Sat F Y
7 6 adantr M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u dom M Sat E Y 1 st u dom N Sat F Y
8 fvex 1 st u V
9 eldm2g 1 st u V 1 st u dom N Sat F Y s 1 st u s N Sat F Y
10 8 9 ax-mp 1 st u dom N Sat F Y s 1 st u s N Sat F Y
11 simpr M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y 1 st u s N Sat F Y
12 2 ad4antr M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y Rel M Sat E Y
13 1stdm Rel M Sat E Y v M Sat E Y 1 st v dom M Sat E Y
14 12 13 sylancom M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v dom M Sat E Y
15 eleq2 dom M Sat E Y = dom N Sat F Y 1 st v dom M Sat E Y 1 st v dom N Sat F Y
16 15 ad5antlr M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v dom M Sat E Y 1 st v dom N Sat F Y
17 fvex 1 st v V
18 eldm2g 1 st v V 1 st v dom N Sat F Y r 1 st v r N Sat F Y
19 17 18 ax-mp 1 st v dom N Sat F Y r 1 st v r N Sat F Y
20 simpr M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y 1 st v r N Sat F Y
21 vex s V
22 8 21 op1std a = 1 st u s 1 st a = 1 st u
23 22 eqcomd a = 1 st u s 1 st u = 1 st a
24 23 ad3antlr M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y 1 st u = 1 st a
25 vex r V
26 17 25 op1std b = 1 st v r 1 st b = 1 st v
27 26 eqcomd b = 1 st v r 1 st v = 1 st b
28 24 27 oveqan12d M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y b = 1 st v r 1 st u 𝑔 1 st v = 1 st a 𝑔 1 st b
29 28 eqeq2d M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y b = 1 st v r x = 1 st u 𝑔 1 st v x = 1 st a 𝑔 1 st b
30 29 biimpd M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y b = 1 st v r x = 1 st u 𝑔 1 st v x = 1 st a 𝑔 1 st b
31 20 30 rspcimedv M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
32 31 ex M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v r N Sat F Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
33 32 exlimdv M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y r 1 st v r N Sat F Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
34 19 33 syl5bi M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v dom N Sat F Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
35 16 34 sylbid M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y 1 st v dom M Sat E Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
36 14 35 mpd M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
37 36 rexlimdva M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y x = 1 st u 𝑔 1 st v b N Sat F Y x = 1 st a 𝑔 1 st b
38 eqidd a = 1 st u s i = i
39 38 23 goaleq12d a = 1 st u s 𝑔 i 1 st u = 𝑔 i 1 st a
40 39 eqeq2d a = 1 st u s x = 𝑔 i 1 st u x = 𝑔 i 1 st a
41 40 biimpd a = 1 st u s x = 𝑔 i 1 st u x = 𝑔 i 1 st a
42 41 adantl M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s x = 𝑔 i 1 st u x = 𝑔 i 1 st a
43 42 reximdv M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s i ω x = 𝑔 i 1 st u i ω x = 𝑔 i 1 st a
44 37 43 orim12d M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y a = 1 st u s v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
45 11 44 rspcimedv M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
46 45 ex M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u s N Sat F Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
47 46 exlimdv M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y s 1 st u s N Sat F Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
48 10 47 syl5bi M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u dom N Sat F Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
49 7 48 sylbid M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y 1 st u dom M Sat E Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
50 4 49 mpd M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
51 50 rexlimdva M V E W Y ω dom M Sat E Y = dom N Sat F Y u M Sat E Y v M Sat E Y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F Y b N Sat F Y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a