Metamath Proof Explorer


Theorem satffunlem

Description: Lemma for satffunlem1lem1 and satffunlem2lem1 . (Contributed by AV, 27-Oct-2023)

Ref Expression
Assertion satffunlem Fun Z s Z r Z u Z v Z x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = w

Proof

Step Hyp Ref Expression
1 eqtr2 x = 1 st u 𝑔 1 st v x = 1 st s 𝑔 1 st r 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r
2 fvex 1 st u V
3 fvex 1 st v V
4 gonafv 1 st u V 1 st v V 1 st u 𝑔 1 st v = 1 𝑜 1 st u 1 st v
5 2 3 4 mp2an 1 st u 𝑔 1 st v = 1 𝑜 1 st u 1 st v
6 fvex 1 st s V
7 fvex 1 st r V
8 gonafv 1 st s V 1 st r V 1 st s 𝑔 1 st r = 1 𝑜 1 st s 1 st r
9 6 7 8 mp2an 1 st s 𝑔 1 st r = 1 𝑜 1 st s 1 st r
10 5 9 eqeq12i 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r 1 𝑜 1 st u 1 st v = 1 𝑜 1 st s 1 st r
11 1oex 1 𝑜 V
12 opex 1 st u 1 st v V
13 11 12 opth 1 𝑜 1 st u 1 st v = 1 𝑜 1 st s 1 st r 1 𝑜 = 1 𝑜 1 st u 1 st v = 1 st s 1 st r
14 2 3 opth 1 st u 1 st v = 1 st s 1 st r 1 st u = 1 st s 1 st v = 1 st r
15 14 anbi2i 1 𝑜 = 1 𝑜 1 st u 1 st v = 1 st s 1 st r 1 𝑜 = 1 𝑜 1 st u = 1 st s 1 st v = 1 st r
16 10 13 15 3bitri 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r 1 𝑜 = 1 𝑜 1 st u = 1 st s 1 st v = 1 st r
17 funfv1st2nd Fun Z s Z Z 1 st s = 2 nd s
18 17 ex Fun Z s Z Z 1 st s = 2 nd s
19 funfv1st2nd Fun Z r Z Z 1 st r = 2 nd r
20 19 ex Fun Z r Z Z 1 st r = 2 nd r
21 18 20 anim12d Fun Z s Z r Z Z 1 st s = 2 nd s Z 1 st r = 2 nd r
22 funfv1st2nd Fun Z u Z Z 1 st u = 2 nd u
23 22 ex Fun Z u Z Z 1 st u = 2 nd u
24 funfv1st2nd Fun Z v Z Z 1 st v = 2 nd v
25 24 ex Fun Z v Z Z 1 st v = 2 nd v
26 23 25 anim12d Fun Z u Z v Z Z 1 st u = 2 nd u Z 1 st v = 2 nd v
27 fveq2 1 st s = 1 st u Z 1 st s = Z 1 st u
28 27 eqcoms 1 st u = 1 st s Z 1 st s = Z 1 st u
29 28 adantr 1 st u = 1 st s 1 st v = 1 st r Z 1 st s = Z 1 st u
30 29 eqeq1d 1 st u = 1 st s 1 st v = 1 st r Z 1 st s = 2 nd s Z 1 st u = 2 nd s
31 fveq2 1 st r = 1 st v Z 1 st r = Z 1 st v
32 31 eqcoms 1 st v = 1 st r Z 1 st r = Z 1 st v
33 32 adantl 1 st u = 1 st s 1 st v = 1 st r Z 1 st r = Z 1 st v
34 33 eqeq1d 1 st u = 1 st s 1 st v = 1 st r Z 1 st r = 2 nd r Z 1 st v = 2 nd r
35 30 34 anbi12d 1 st u = 1 st s 1 st v = 1 st r Z 1 st s = 2 nd s Z 1 st r = 2 nd r Z 1 st u = 2 nd s Z 1 st v = 2 nd r
36 35 anbi1d 1 st u = 1 st s 1 st v = 1 st r Z 1 st s = 2 nd s Z 1 st r = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v Z 1 st u = 2 nd s Z 1 st v = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v
37 eqtr2 Z 1 st u = 2 nd s Z 1 st u = 2 nd u 2 nd s = 2 nd u
38 37 ad2ant2r Z 1 st u = 2 nd s Z 1 st v = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v 2 nd s = 2 nd u
39 eqtr2 Z 1 st v = 2 nd r Z 1 st v = 2 nd v 2 nd r = 2 nd v
40 39 ad2ant2l Z 1 st u = 2 nd s Z 1 st v = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v 2 nd r = 2 nd v
41 38 40 ineq12d Z 1 st u = 2 nd s Z 1 st v = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v 2 nd s 2 nd r = 2 nd u 2 nd v
42 36 41 syl6bi 1 st u = 1 st s 1 st v = 1 st r Z 1 st s = 2 nd s Z 1 st r = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v 2 nd s 2 nd r = 2 nd u 2 nd v
43 42 com12 Z 1 st s = 2 nd s Z 1 st r = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v 1 st u = 1 st s 1 st v = 1 st r 2 nd s 2 nd r = 2 nd u 2 nd v
44 43 a1i Fun Z Z 1 st s = 2 nd s Z 1 st r = 2 nd r Z 1 st u = 2 nd u Z 1 st v = 2 nd v 1 st u = 1 st s 1 st v = 1 st r 2 nd s 2 nd r = 2 nd u 2 nd v
45 21 26 44 syl2and Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r 2 nd s 2 nd r = 2 nd u 2 nd v
46 45 expd Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r 2 nd s 2 nd r = 2 nd u 2 nd v
47 46 3imp1 Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r 2 nd s 2 nd r = 2 nd u 2 nd v
48 47 difeq2d Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r M ω 2 nd s 2 nd r = M ω 2 nd u 2 nd v
49 48 adantr Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v M ω 2 nd s 2 nd r = M ω 2 nd u 2 nd v
50 eqeq12 y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w M ω 2 nd s 2 nd r = M ω 2 nd u 2 nd v
51 50 adantl Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w M ω 2 nd s 2 nd r = M ω 2 nd u 2 nd v
52 49 51 mpbird Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w
53 52 exp43 Fun Z s Z r Z u Z v Z 1 st u = 1 st s 1 st v = 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w
54 53 adantld Fun Z s Z r Z u Z v Z 1 𝑜 = 1 𝑜 1 st u = 1 st s 1 st v = 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w
55 16 54 syl5bi Fun Z s Z r Z u Z v Z 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w
56 1 55 syl5 Fun Z s Z r Z u Z v Z x = 1 st u 𝑔 1 st v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w
57 56 expd Fun Z s Z r Z u Z v Z x = 1 st u 𝑔 1 st v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r w = M ω 2 nd u 2 nd v y = w
58 57 com35 Fun Z s Z r Z u Z v Z x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = M ω 2 nd s 2 nd r x = 1 st s 𝑔 1 st r y = w
59 58 impd Fun Z s Z r Z u Z v Z x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = M ω 2 nd s 2 nd r x = 1 st s 𝑔 1 st r y = w
60 59 com24 Fun Z s Z r Z u Z v Z x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = w
61 60 impd Fun Z s Z r Z u Z v Z x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = w
62 61 3imp Fun Z s Z r Z u Z v Z x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = w