Metamath Proof Explorer


Theorem satfv1

Description: The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023)

Ref Expression
Hypothesis satfv1.s S = M Sat E
Assertion satfv1 M V E W S 1 𝑜 = S x y | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j

Proof

Step Hyp Ref Expression
1 satfv1.s S = M Sat E
2 df-1o 1 𝑜 = suc
3 2 fveq2i S 1 𝑜 = S suc
4 3 a1i M V E W S 1 𝑜 = S suc
5 peano1 ω
6 1 satfvsuc M V E W ω S suc = S x y | o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o
7 5 6 mp3an3 M V E W S suc = S x y | o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o
8 1 satfv0 M V E W S = e b | i ω j ω e = i 𝑔 j b = a M ω | a i E a j
9 8 rexeqdv M V E W o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o o e b | i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o
10 eqid e b | i ω j ω e = i 𝑔 j b = a M ω | a i E a j = e b | i ω j ω e = i 𝑔 j b = a M ω | a i E a j
11 vex e V
12 vex b V
13 11 12 op1std o = e b 1 st o = e
14 13 oveq1d o = e b 1 st o 𝑔 1 st p = e 𝑔 1 st p
15 14 eqeq2d o = e b x = 1 st o 𝑔 1 st p x = e 𝑔 1 st p
16 11 12 op2ndd o = e b 2 nd o = b
17 16 ineq1d o = e b 2 nd o 2 nd p = b 2 nd p
18 17 difeq2d o = e b M ω 2 nd o 2 nd p = M ω b 2 nd p
19 18 eqeq2d o = e b y = M ω 2 nd o 2 nd p y = M ω b 2 nd p
20 15 19 anbi12d o = e b x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p x = e 𝑔 1 st p y = M ω b 2 nd p
21 20 rexbidv o = e b p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p p S x = e 𝑔 1 st p y = M ω b 2 nd p
22 eqidd o = e b n = n
23 22 13 goaleq12d o = e b 𝑔 n 1 st o = 𝑔 n e
24 23 eqeq2d o = e b x = 𝑔 n 1 st o x = 𝑔 n e
25 16 eleq2d o = e b n z a ω n 2 nd o n z a ω n b
26 25 ralbidv o = e b z M n z a ω n 2 nd o z M n z a ω n b
27 26 rabbidv o = e b a M ω | z M n z a ω n 2 nd o = a M ω | z M n z a ω n b
28 27 eqeq2d o = e b y = a M ω | z M n z a ω n 2 nd o y = a M ω | z M n z a ω n b
29 24 28 anbi12d o = e b x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o x = 𝑔 n e y = a M ω | z M n z a ω n b
30 29 rexbidv o = e b n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
31 21 30 orbi12d o = e b p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
32 10 31 rexopabb o e b | i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
33 9 32 bitrdi M V E W o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
34 1 satfv0 M V E W S = c d | k ω l ω c = k 𝑔 l d = a M ω | a k E a l
35 34 rexeqdv M V E W p S x = e 𝑔 1 st p y = M ω b 2 nd p p c d | k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 1 st p y = M ω b 2 nd p
36 eqid c d | k ω l ω c = k 𝑔 l d = a M ω | a k E a l = c d | k ω l ω c = k 𝑔 l d = a M ω | a k E a l
37 vex c V
38 vex d V
39 37 38 op1std p = c d 1 st p = c
40 39 oveq2d p = c d e 𝑔 1 st p = e 𝑔 c
41 40 eqeq2d p = c d x = e 𝑔 1 st p x = e 𝑔 c
42 37 38 op2ndd p = c d 2 nd p = d
43 42 ineq2d p = c d b 2 nd p = b d
44 43 difeq2d p = c d M ω b 2 nd p = M ω b d
45 44 eqeq2d p = c d y = M ω b 2 nd p y = M ω b d
46 41 45 anbi12d p = c d x = e 𝑔 1 st p y = M ω b 2 nd p x = e 𝑔 c y = M ω b d
47 36 46 rexopabb p c d | k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 1 st p y = M ω b 2 nd p c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d
48 35 47 bitrdi M V E W p S x = e 𝑔 1 st p y = M ω b 2 nd p c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d
49 48 orbi1d M V E W p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
50 49 anbi2d M V E W i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
51 50 2exbidv M V E W e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
52 r19.41vv i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
53 oveq1 e = i 𝑔 j e 𝑔 c = i 𝑔 j 𝑔 c
54 53 eqeq2d e = i 𝑔 j x = e 𝑔 c x = i 𝑔 j 𝑔 c
55 ineq1 b = a M ω | a i E a j b d = a M ω | a i E a j d
56 55 difeq2d b = a M ω | a i E a j M ω b d = M ω a M ω | a i E a j d
57 56 eqeq2d b = a M ω | a i E a j y = M ω b d y = M ω a M ω | a i E a j d
58 54 57 bi2anan9 e = i 𝑔 j b = a M ω | a i E a j x = e 𝑔 c y = M ω b d x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
59 58 anbi2d e = i 𝑔 j b = a M ω | a i E a j k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
60 59 2exbidv e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
61 eqidd e = i 𝑔 j n = n
62 id e = i 𝑔 j e = i 𝑔 j
63 61 62 goaleq12d e = i 𝑔 j 𝑔 n e = 𝑔 n i 𝑔 j
64 63 eqeq2d e = i 𝑔 j x = 𝑔 n e x = 𝑔 n i 𝑔 j
65 nfrab1 _ a a M ω | a i E a j
66 65 nfeq2 a b = a M ω | a i E a j
67 eleq2 b = a M ω | a i E a j n z a ω n b n z a ω n a M ω | a i E a j
68 67 ralbidv b = a M ω | a i E a j z M n z a ω n b z M n z a ω n a M ω | a i E a j
69 66 68 rabbid b = a M ω | a i E a j a M ω | z M n z a ω n b = a M ω | z M n z a ω n a M ω | a i E a j
70 69 eqeq2d b = a M ω | a i E a j y = a M ω | z M n z a ω n b y = a M ω | z M n z a ω n a M ω | a i E a j
71 64 70 bi2anan9 e = i 𝑔 j b = a M ω | a i E a j x = 𝑔 n e y = a M ω | z M n z a ω n b x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
72 71 rexbidv e = i 𝑔 j b = a M ω | a i E a j n ω x = 𝑔 n e y = a M ω | z M n z a ω n b n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
73 60 72 orbi12d e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
74 73 adantl i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
75 r19.41vv k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
76 oveq2 c = k 𝑔 l i 𝑔 j 𝑔 c = i 𝑔 j 𝑔 k 𝑔 l
77 76 adantr c = k 𝑔 l d = a M ω | a k E a l i 𝑔 j 𝑔 c = i 𝑔 j 𝑔 k 𝑔 l
78 77 eqeq2d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c x = i 𝑔 j 𝑔 k 𝑔 l
79 ineq2 d = a M ω | a k E a l a M ω | a i E a j d = a M ω | a i E a j a M ω | a k E a l
80 79 difeq2d d = a M ω | a k E a l M ω a M ω | a i E a j d = M ω a M ω | a i E a j a M ω | a k E a l
81 inrab a M ω | a i E a j a M ω | a k E a l = a M ω | a i E a j a k E a l
82 81 difeq2i M ω a M ω | a i E a j a M ω | a k E a l = M ω a M ω | a i E a j a k E a l
83 notrab M ω a M ω | a i E a j a k E a l = a M ω | ¬ a i E a j a k E a l
84 ianor ¬ a i E a j a k E a l ¬ a i E a j ¬ a k E a l
85 84 rabbii a M ω | ¬ a i E a j a k E a l = a M ω | ¬ a i E a j ¬ a k E a l
86 82 83 85 3eqtri M ω a M ω | a i E a j a M ω | a k E a l = a M ω | ¬ a i E a j ¬ a k E a l
87 80 86 eqtrdi d = a M ω | a k E a l M ω a M ω | a i E a j d = a M ω | ¬ a i E a j ¬ a k E a l
88 87 eqeq2d d = a M ω | a k E a l y = M ω a M ω | a i E a j d y = a M ω | ¬ a i E a j ¬ a k E a l
89 88 adantl c = k 𝑔 l d = a M ω | a k E a l y = M ω a M ω | a i E a j d y = a M ω | ¬ a i E a j ¬ a k E a l
90 78 89 anbi12d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
91 90 biimpa c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
92 91 reximi l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
93 92 reximi k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
94 75 93 sylbir k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
95 94 exlimivv c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
96 95 a1i i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l
97 simpr i ω j ω n ω n ω
98 simpll i ω j ω n ω i ω
99 simplr i ω j ω n ω j ω
100 fveq1 a = b a i = b i
101 fveq1 a = b a j = b j
102 100 101 breq12d a = b a i E a j b i E b j
103 102 cbvrabv a M ω | a i E a j = b M ω | b i E b j
104 103 eleq2i n z a ω n a M ω | a i E a j n z a ω n b M ω | b i E b j
105 104 ralbii z M n z a ω n a M ω | a i E a j z M n z a ω n b M ω | b i E b j
106 105 rabbii a M ω | z M n z a ω n a M ω | a i E a j = a M ω | z M n z a ω n b M ω | b i E b j
107 satfv1lem n ω i ω j ω a M ω | z M n z a ω n b M ω | b i E b j = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
108 106 107 syl5eq n ω i ω j ω a M ω | z M n z a ω n a M ω | a i E a j = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
109 97 98 99 108 syl3anc i ω j ω n ω a M ω | z M n z a ω n a M ω | a i E a j = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
110 109 eqeq2d i ω j ω n ω y = a M ω | z M n z a ω n a M ω | a i E a j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
111 110 biimpd i ω j ω n ω y = a M ω | z M n z a ω n a M ω | a i E a j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
112 111 anim2d i ω j ω n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
113 112 reximdva i ω j ω n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
114 113 adantr i ω j ω e = i 𝑔 j b = a M ω | a i E a j n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
115 96 114 orim12d i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
116 74 115 sylbid i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
117 116 expimpd i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
118 117 reximdva i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
119 118 reximia i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
120 52 119 sylbir i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
121 120 exlimivv e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
122 ovex i 𝑔 j V
123 ovex M ω V
124 123 rabex a M ω | a i E a j V
125 122 124 pm3.2i i 𝑔 j V a M ω | a i E a j V
126 eqid k 𝑔 l = k 𝑔 l
127 eqid a M ω | a k E a l = a M ω | a k E a l
128 126 127 pm3.2i k 𝑔 l = k 𝑔 l a M ω | a k E a l = a M ω | a k E a l
129 86 eqcomi a M ω | ¬ a i E a j ¬ a k E a l = M ω a M ω | a i E a j a M ω | a k E a l
130 129 eqeq2i y = a M ω | ¬ a i E a j ¬ a k E a l y = M ω a M ω | a i E a j a M ω | a k E a l
131 130 biimpi y = a M ω | ¬ a i E a j ¬ a k E a l y = M ω a M ω | a i E a j a M ω | a k E a l
132 131 anim2i x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l x = i 𝑔 j 𝑔 k 𝑔 l y = M ω a M ω | a i E a j a M ω | a k E a l
133 ovex k 𝑔 l V
134 123 rabex a M ω | a k E a l V
135 eqeq1 c = k 𝑔 l c = k 𝑔 l k 𝑔 l = k 𝑔 l
136 eqeq1 d = a M ω | a k E a l d = a M ω | a k E a l a M ω | a k E a l = a M ω | a k E a l
137 135 136 bi2anan9 c = k 𝑔 l d = a M ω | a k E a l c = k 𝑔 l d = a M ω | a k E a l k 𝑔 l = k 𝑔 l a M ω | a k E a l = a M ω | a k E a l
138 76 eqeq2d c = k 𝑔 l x = i 𝑔 j 𝑔 c x = i 𝑔 j 𝑔 k 𝑔 l
139 80 eqeq2d d = a M ω | a k E a l y = M ω a M ω | a i E a j d y = M ω a M ω | a i E a j a M ω | a k E a l
140 138 139 bi2anan9 c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d x = i 𝑔 j 𝑔 k 𝑔 l y = M ω a M ω | a i E a j a M ω | a k E a l
141 137 140 anbi12d c = k 𝑔 l d = a M ω | a k E a l c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k 𝑔 l = k 𝑔 l a M ω | a k E a l = a M ω | a k E a l x = i 𝑔 j 𝑔 k 𝑔 l y = M ω a M ω | a i E a j a M ω | a k E a l
142 133 134 141 spc2ev k 𝑔 l = k 𝑔 l a M ω | a k E a l = a M ω | a k E a l x = i 𝑔 j 𝑔 k 𝑔 l y = M ω a M ω | a i E a j a M ω | a k E a l c d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
143 128 132 142 sylancr x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l c d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
144 143 reximi l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l l ω c d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
145 144 reximi k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l k ω l ω c d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
146 75 bicomi k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
147 146 2exbii c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
148 2ex2rexrot c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω c d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
149 147 148 bitri c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d k ω l ω c d c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
150 145 149 sylibr k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
151 150 a1i i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d
152 109 eqcomd i ω j ω n ω a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j = a M ω | z M n z a ω n a M ω | a i E a j
153 152 eqeq2d i ω j ω n ω y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j y = a M ω | z M n z a ω n a M ω | a i E a j
154 153 biimpd i ω j ω n ω y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j y = a M ω | z M n z a ω n a M ω | a i E a j
155 154 anim2d i ω j ω n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
156 155 reximdva i ω j ω n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
157 151 156 orim12d i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
158 157 imp i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
159 eqid i 𝑔 j = i 𝑔 j
160 eqid a M ω | a i E a j = a M ω | a i E a j
161 159 160 pm3.2i i 𝑔 j = i 𝑔 j a M ω | a i E a j = a M ω | a i E a j
162 158 161 jctil i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j i 𝑔 j = i 𝑔 j a M ω | a i E a j = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
163 eqeq1 e = i 𝑔 j e = i 𝑔 j i 𝑔 j = i 𝑔 j
164 eqeq1 b = a M ω | a i E a j b = a M ω | a i E a j a M ω | a i E a j = a M ω | a i E a j
165 163 164 bi2anan9 e = i 𝑔 j b = a M ω | a i E a j e = i 𝑔 j b = a M ω | a i E a j i 𝑔 j = i 𝑔 j a M ω | a i E a j = a M ω | a i E a j
166 165 73 anbi12d e = i 𝑔 j b = a M ω | a i E a j e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i 𝑔 j = i 𝑔 j a M ω | a i E a j = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j
167 166 spc2egv i 𝑔 j V a M ω | a i E a j V i 𝑔 j = i 𝑔 j a M ω | a i E a j = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = i 𝑔 j 𝑔 c y = M ω a M ω | a i E a j d n ω x = 𝑔 n i 𝑔 j y = a M ω | z M n z a ω n a M ω | a i E a j e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
168 125 162 167 mpsyl i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
169 168 ex i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
170 169 reximdva i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j j ω e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
171 170 reximia i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j i ω j ω e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
172 52 bicomi i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
173 172 2exbii e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
174 2ex2rexrot e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
175 173 174 bitri e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω e b e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
176 171 175 sylibr i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b
177 121 176 impbii e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j c d k ω l ω c = k 𝑔 l d = a M ω | a k E a l x = e 𝑔 c y = M ω b d n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
178 51 177 bitrdi M V E W e b i ω j ω e = i 𝑔 j b = a M ω | a i E a j p S x = e 𝑔 1 st p y = M ω b 2 nd p n ω x = 𝑔 n e y = a M ω | z M n z a ω n b i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
179 33 178 bitrd M V E W o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
180 179 opabbidv M V E W x y | o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o = x y | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
181 180 uneq2d M V E W S x y | o S p S x = 1 st o 𝑔 1 st p y = M ω 2 nd o 2 nd p n ω x = 𝑔 n 1 st o y = a M ω | z M n z a ω n 2 nd o = S x y | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j
182 4 7 181 3eqtrd M V E W S 1 𝑜 = S x y | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l y = a M ω | ¬ a i E a j ¬ a k E a l n ω x = 𝑔 n i 𝑔 j y = a M ω | z M if- i = n if- j = n z E z z E a j if- j = n a i E z a i E a j