Metamath Proof Explorer


Theorem satfvsuclem2

Description: Lemma 2 for satfvsuc . (Contributed by AV, 8-Oct-2023)

Ref Expression
Hypothesis satfv0.s S = M Sat E
Assertion satfvsuclem2 M V E W N ω x y | u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u V

Proof

Step Hyp Ref Expression
1 satfv0.s S = M Sat E
2 r19.41v v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω
3 r19.41v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
4 2 3 orbi12i v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
5 ovex M ω V
6 difelpw M ω V M ω 2 nd u 2 nd v 𝒫 M ω
7 5 6 ax-mp M ω 2 nd u 2 nd v 𝒫 M ω
8 eleq1 y = M ω 2 nd u 2 nd v y 𝒫 M ω M ω 2 nd u 2 nd v 𝒫 M ω
9 7 8 mpbiri y = M ω 2 nd u 2 nd v y 𝒫 M ω
10 9 pm4.71i y = M ω 2 nd u 2 nd v y = M ω 2 nd u 2 nd v y 𝒫 M ω
11 10 bianass x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω
12 11 rexbii v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω
13 rabelpw M ω V a M ω | z M i z a ω i 2 nd u 𝒫 M ω
14 5 13 ax-mp a M ω | z M i z a ω i 2 nd u 𝒫 M ω
15 eleq1 y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω a M ω | z M i z a ω i 2 nd u 𝒫 M ω
16 14 15 mpbiri y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
17 16 pm4.71i y = a M ω | z M i z a ω i 2 nd u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
18 17 bianass x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
19 18 rexbii i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
20 12 19 orbi12i v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
21 andir v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v y 𝒫 M ω i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
22 4 20 21 3bitr4i v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
23 22 rexbii u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
24 r19.41v u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
25 23 24 bitri u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
26 25 opabbii x y | u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u = x y | u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω
27 1 satfvsuclem1 M V E W N ω x y | u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u y 𝒫 M ω V
28 26 27 eqeltrid M V E W N ω x y | u S N v S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u V