Metamath Proof Explorer


Theorem satfvsucsuc

Description: The satisfaction predicate as function over wff codes of height ( N + 1 ) , expressed by the minimally necessary satisfaction predicates as function over wff codes of height N . (Contributed by AV, 21-Oct-2023)

Ref Expression
Hypotheses satfvsucsuc.s S = M Sat E
satfvsucsuc.a A = M ω 2 nd u 2 nd v
satfvsucsuc.b B = a M ω | z M i z a ω i 2 nd u
Assertion satfvsucsuc M V E W N ω S suc suc N = S suc N x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A

Proof

Step Hyp Ref Expression
1 satfvsucsuc.s S = M Sat E
2 satfvsucsuc.a A = M ω 2 nd u 2 nd v
3 satfvsucsuc.b B = a M ω | z M i z a ω i 2 nd u
4 peano2 N ω suc N ω
5 1 satfvsuc M V E W suc N ω S suc suc N = S suc N x y | u S suc N v S suc 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
6 4 5 syl3an3 M V E W N ω S suc suc N = S suc N x y | u S suc N v S suc 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
7 orc s S suc N s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
8 7 a1i M V E W N ω s S suc N s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
9 2 eqeq2i y = A y = M ω 2 nd u 2 nd v
10 9 anbi2i x = 1 st u 𝑔 1 st v y = A x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
11 10 rexbii v S suc N x = 1 st u 𝑔 1 st v y = A v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
12 3 eqeq2i y = B y = a M ω | z M i z a ω i 2 nd u
13 12 anbi2i x = 𝑔 i 1 st u y = B x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
14 13 rexbii i ω x = 𝑔 i 1 st u y = B i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
15 11 14 orbi12i v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B v S suc 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
16 15 rexbii u S suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N v S suc 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
17 16 bicomi u S suc N v S suc 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 suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
18 3simpa M V E W N ω M V E W
19 4 ancri N ω suc N ω N ω
20 19 3ad2ant3 M V E W N ω suc N ω N ω
21 18 20 jca M V E W N ω M V E W suc N ω N ω
22 sssucid N suc N
23 22 a1i M V E W N ω s = x y N suc N
24 1 satfsschain M V E W suc N ω N ω N suc N S N S suc N
25 24 imp M V E W suc N ω N ω N suc N S N S suc N
26 21 23 25 syl2an2r M V E W N ω s = x y S N S suc N
27 undif S N S suc N S N S suc N S N = S suc N
28 26 27 sylib M V E W N ω s = x y S N S suc N S N = S suc N
29 28 eqcomd M V E W N ω s = x y S suc N = S N S suc N S N
30 29 rexeqdv M V E W N ω s = x y u S suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
31 rexun u S N S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
32 30 31 bitrdi M V E W N ω s = x y u S suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
33 17 32 syl5bb M V E W N ω s = x y u S suc N v S suc 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 suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
34 r19.43 u S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B
35 22 a1i M V E W N ω N suc N
36 21 35 jca M V E W N ω M V E W suc N ω N ω N suc N
37 36 25 syl M V E W N ω S N S suc N
38 37 adantr M V E W N ω s = x y S N S suc N
39 38 27 sylib M V E W N ω s = x y S N S suc N S N = S suc N
40 39 eqcomd M V E W N ω s = x y S suc N = S N S suc N S N
41 40 rexeqdv M V E W N ω s = x y v S suc N x = 1 st u 𝑔 1 st v y = A v S N S suc N S N x = 1 st u 𝑔 1 st v y = A
42 rexun v S N S suc N S N x = 1 st u 𝑔 1 st v y = A v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A
43 41 42 bitrdi M V E W N ω s = x y v S suc N x = 1 st u 𝑔 1 st v y = A v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A
44 43 rexbidv M V E W N ω s = x y u S N v S suc N x = 1 st u 𝑔 1 st v y = A u S N v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A
45 44 orbi1d M V E W N ω s = x y u S N v S suc N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B
46 r19.43 u S N v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N v S N x = 1 st u 𝑔 1 st v y = A u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
47 46 orbi1i u S N v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B
48 or32 u S N v S N x = 1 st u 𝑔 1 st v y = A u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
49 r19.43 u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B
50 49 bicomi u S N v S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
51 50 orbi1i u S N v S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
52 48 51 bitri u S N v S N x = 1 st u 𝑔 1 st v y = A u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
53 47 52 bitri u S N v S N x = 1 st u 𝑔 1 st v y = A v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
54 45 53 bitrdi M V E W N ω s = x y u S N v S suc N x = 1 st u 𝑔 1 st v y = A u S N i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
55 34 54 syl5bb M V E W N ω s = x y u S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
56 animorr M V E W N ω s = x y u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B x y S N u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
57 1 satfvsuc M V E W N ω S suc N = S 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
58 57 eleq2d M V E W N ω s S suc N s S 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
59 58 adantr M V E W N ω s = x y s S suc N s S 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
60 eleq1 s = x y s S 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 x y S 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
61 60 adantl M V E W N ω s = x y s S 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 x y S 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
62 elun x y S 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 x y S N x y 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
63 opabidw x y 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 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
64 63 orbi2i x y S N x y 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 S N 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
65 62 64 bitri x y S 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 x y S N 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
66 61 65 bitrdi M V E W N ω s = x y s S 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 x y S N 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
67 59 66 bitrd M V E W N ω s = x y s S suc N x y S N 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
68 2 eqcomi M ω 2 nd u 2 nd v = A
69 68 eqeq2i y = M ω 2 nd u 2 nd v y = A
70 69 anbi2i x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v y = A
71 70 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 = A
72 3 eqcomi a M ω | z M i z a ω i 2 nd u = B
73 72 eqeq2i y = a M ω | z M i z a ω i 2 nd u y = B
74 73 anbi2i x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x = 𝑔 i 1 st u y = B
75 74 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 = B
76 71 75 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 = A i ω x = 𝑔 i 1 st u y = B
77 76 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 = A i ω x = 𝑔 i 1 st u y = B
78 77 a1i M V E W N ω s = 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 u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
79 78 orbi2d M V E W N ω s = x y x y S N 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 S N u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
80 67 79 bitrd M V E W N ω s = x y s S suc N x y S N u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
81 80 adantr M V E W N ω s = x y u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N x y S N u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
82 56 81 mpbird M V E W N ω s = x y u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N
83 82 orcd M V E W N ω s = x y u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
84 83 ex M V E W N ω s = x y u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
85 simplr M V E W N ω s = x y u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s = x y
86 animorr M V E W N ω s = x y u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
87 85 86 jca M V E W N ω s = x y u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
88 87 olcd M V E W N ω s = x y u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
89 88 ex M V E W N ω s = x y u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
90 84 89 jaod M V E W N ω s = x y u S N v S N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
91 55 90 sylbid M V E W N ω s = x y u S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
92 simplr M V E W N ω s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s = x y
93 orc u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
94 93 adantl M V E W N ω s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
95 92 94 jca M V E W N ω s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
96 95 olcd M V E W N ω s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
97 96 ex M V E W N ω s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
98 91 97 jaod M V E W N ω s = x y u S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
99 33 98 sylbid M V E W N ω s = x y u S suc N v S suc 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 s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
100 99 expimpd M V E W N ω s = x y u S suc N v S suc 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 s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
101 100 2eximdv M V E W N ω x y s = x y u S suc N v S suc 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 s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
102 19.45v y s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
103 102 exbii x y s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A x s S suc N y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
104 19.45v x s S suc N y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
105 103 104 bitri x y s S suc N s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
106 101 105 syl6ib M V E W N ω x y s = x y u S suc N v S suc 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 s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
107 8 106 jaod M V E W N ω s S suc N x y s = x y u S suc N v S suc 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 s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
108 difss S suc N S N S suc N
109 ssrexv S suc N S N S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
110 108 109 ax-mp u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
111 110 a1i M V E W N ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B
112 111 16 syl6ib M V E W N ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N v S suc 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
113 ssrexv S N S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = A
114 37 113 syl M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = A
115 10 2rexbii u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
116 114 115 syl6ib M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
117 116 imp M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
118 ssrexv S suc N S N S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
119 108 118 ax-mp v S suc N S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
120 119 reximi u S suc N v S suc N S N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v u S suc N v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
121 117 120 syl M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v
122 121 orcd M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v u S suc N i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
123 122 ex M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v u S suc N i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
124 r19.43 u S suc N v S suc 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 suc N v S suc N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v u S suc N i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
125 123 124 syl6ibr M V E W N ω u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc 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
126 112 125 jaod M V E W N ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N v S suc 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
127 126 anim2d M V E W N ω s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s = x y u S suc N v S suc 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
128 127 2eximdv M V E W N ω x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A x y s = x y u S suc N v S suc 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
129 128 orim2d M V E W N ω s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N x y s = x y u S suc N v S suc 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
130 107 129 impbid M V E W N ω s S suc N x y s = x y u S suc N v S suc 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 s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
131 elun s S suc N x y | u S suc N v S suc 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 s S suc N s x y | u S suc N v S suc 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
132 elopab s x y | u S suc N v S suc 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 s = x y u S suc N v S suc 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
133 132 orbi2i s S suc N s x y | u S suc N v S suc 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 s S suc N x y s = x y u S suc N v S suc 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
134 131 133 bitri s S suc N x y | u S suc N v S suc 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 s S suc N x y s = x y u S suc N v S suc 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
135 elun s S suc N x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N s x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
136 elopab s x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
137 136 orbi2i s S suc N s x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
138 135 137 bitri s S suc N x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N x y s = x y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
139 130 134 138 3bitr4g M V E W N ω s S suc N x y | u S suc N v S suc 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 s S suc N x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
140 139 eqrdv M V E W N ω S suc N x y | u S suc N v S suc 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 = S suc N x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
141 6 140 eqtrd M V E W N ω S suc suc N = S suc N x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A