Metamath Proof Explorer


Theorem satfv1lem

Description: Lemma for satfv1 . (Contributed by AV, 9-Nov-2023)

Ref Expression
Assertion satfv1lem NωIωJωaMω|zMNzaωNbMω|bIEbJ=aMω|zMif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ

Proof

Step Hyp Ref Expression
1 fveq1 b=NzaωNbI=NzaωNI
2 fveq1 b=NzaωNbJ=NzaωNJ
3 1 2 breq12d b=NzaωNbIEbJNzaωNIENzaωNJ
4 3 elrab NzaωNbMω|bIEbJNzaωNMωNzaωNIENzaωNJ
5 4 a1i NωIωJωaMωzMNzaωNbMω|bIEbJNzaωNMωNzaωNIENzaωNJ
6 elex NωNV
7 6 3ad2ant1 NωIωJωNV
8 7 ad2antrr NωIωJωaMωzMNV
9 simpr NωIωJωaMωzMzM
10 8 9 fsnd NωIωJωaMωzMNz:NM
11 elmapex aMωMVωV
12 11 simpld aMωMV
13 12 adantr aMωzMMV
14 snex NV
15 14 a1i aMωzMNV
16 13 15 elmapd aMωzMNzMNNz:NM
17 16 adantll NωIωJωaMωzMNzMNNz:NM
18 10 17 mpbird NωIωJωaMωzMNzMN
19 elmapi aMωa:ωM
20 difssd aMωωNω
21 19 20 fssresd aMωaωN:ωNM
22 omex ωV
23 22 difexi ωNV
24 23 a1i aMωωNV
25 12 24 elmapd aMωaωNMωNaωN:ωNM
26 21 25 mpbird aMωaωNMωN
27 26 adantl NωIωJωaMωaωNMωN
28 27 adantr NωIωJωaMωzMaωNMωN
29 res0 Nz=
30 res0 aωN=
31 29 30 eqtr4i Nz=aωN
32 disjdif NωN=
33 32 reseq2i NzNωN=Nz
34 32 reseq2i aωNNωN=aωN
35 31 33 34 3eqtr4i NzNωN=aωNNωN
36 35 a1i NωIωJωaMωzMNzNωN=aωNNωN
37 elmapresaun NzMNaωNMωNNzNωN=aωNNωNNzaωNMNωN
38 18 28 36 37 syl3anc NωIωJωaMωzMNzaωNMNωN
39 uncom NωN=ωNN
40 difsnid NωωNN=ω
41 39 40 eqtr2id Nωω=NωN
42 41 3ad2ant1 NωIωJωω=NωN
43 42 ad2antrr NωIωJωaMωzMω=NωN
44 43 oveq2d NωIωJωaMωzMMω=MNωN
45 38 44 eleqtrrd NωIωJωaMωzMNzaωNMω
46 ibar NzaωNMωNzaωNIENzaωNJNzaωNMωNzaωNIENzaωNJ
47 46 adantl NωIωJωaMωzMNzaωNMωNzaωNIENzaωNJNzaωNMωNzaωNIENzaωNJ
48 47 bicomd NωIωJωaMωzMNzaωNMωNzaωNMωNzaωNIENzaωNJNzaωNIENzaωNJ
49 simpll1 NωIωJωaMωzMNω
50 eqid NzaωN=NzaωN
51 49 9 50 fvsnun1 NωIωJωaMωzMNzaωNN=z
52 51 adantr NωIωJωaMωzMNzaωNMωNzaωNN=z
53 52 52 breq12d NωIωJωaMωzMNzaωNMωNzaωNNENzaωNNzEz
54 53 adantl J=NNωIωJωaMωzMNzaωNMωNzaωNNENzaωNNzEz
55 fveq2 J=NNzaωNJ=NzaωNN
56 55 breq2d J=NNzaωNNENzaωNJNzaωNNENzaωNN
57 ifptru J=Nif-J=NzEzzEaJzEz
58 56 57 bibi12d J=NNzaωNNENzaωNJif-J=NzEzzEaJNzaωNNENzaωNNzEz
59 58 adantr J=NNωIωJωaMωzMNzaωNMωNzaωNNENzaωNJif-J=NzEzzEaJNzaωNNENzaωNNzEz
60 54 59 mpbird J=NNωIωJωaMωzMNzaωNMωNzaωNNENzaωNJif-J=NzEzzEaJ
61 52 adantl ¬J=NNωIωJωaMωzMNzaωNMωNzaωNN=z
62 49 adantr NωIωJωaMωzMNzaωNMωNω
63 62 adantl ¬J=NNωIωJωaMωzMNzaωNMωNω
64 9 adantr NωIωJωaMωzMNzaωNMωzM
65 64 adantl ¬J=NNωIωJωaMωzMNzaωNMωzM
66 neqne ¬J=NJN
67 simpll3 NωIωJωaMωzMJω
68 67 adantr NωIωJωaMωzMNzaωNMωJω
69 66 68 anim12ci ¬J=NNωIωJωaMωzMNzaωNMωJωJN
70 eldifsn JωNJωJN
71 69 70 sylibr ¬J=NNωIωJωaMωzMNzaωNMωJωN
72 63 65 50 71 fvsnun2 ¬J=NNωIωJωaMωzMNzaωNMωNzaωNJ=aJ
73 61 72 breq12d ¬J=NNωIωJωaMωzMNzaωNMωNzaωNNENzaωNJzEaJ
74 ifpfal ¬J=Nif-J=NzEzzEaJzEaJ
75 74 bicomd ¬J=NzEaJif-J=NzEzzEaJ
76 75 adantr ¬J=NNωIωJωaMωzMNzaωNMωzEaJif-J=NzEzzEaJ
77 73 76 bitrd ¬J=NNωIωJωaMωzMNzaωNMωNzaωNNENzaωNJif-J=NzEzzEaJ
78 60 77 pm2.61ian NωIωJωaMωzMNzaωNMωNzaωNNENzaωNJif-J=NzEzzEaJ
79 78 adantl I=NNωIωJωaMωzMNzaωNMωNzaωNNENzaωNJif-J=NzEzzEaJ
80 fveq2 I=NNzaωNI=NzaωNN
81 80 breq1d I=NNzaωNIENzaωNJNzaωNNENzaωNJ
82 ifptru I=Nif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJif-J=NzEzzEaJ
83 81 82 bibi12d I=NNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJNzaωNNENzaωNJif-J=NzEzzEaJ
84 83 adantr I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJNzaωNNENzaωNJif-J=NzEzzEaJ
85 79 84 mpbird I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
86 62 adantl ¬I=NNωIωJωaMωzMNzaωNMωNω
87 64 adantl ¬I=NNωIωJωaMωzMNzaωNMωzM
88 neqne ¬I=NIN
89 simpll2 NωIωJωaMωzMIω
90 89 adantr NωIωJωaMωzMNzaωNMωIω
91 88 90 anim12ci ¬I=NNωIωJωaMωzMNzaωNMωIωIN
92 eldifsn IωNIωIN
93 91 92 sylibr ¬I=NNωIωJωaMωzMNzaωNMωIωN
94 86 87 50 93 fvsnun2 ¬I=NNωIωJωaMωzMNzaωNMωNzaωNI=aI
95 52 adantl ¬I=NNωIωJωaMωzMNzaωNMωNzaωNN=z
96 94 95 breq12d ¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNNaIEz
97 96 adantl J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNNaIEz
98 55 breq2d J=NNzaωNIENzaωNJNzaωNIENzaωNN
99 ifptru J=Nif-J=NaIEzaIEaJaIEz
100 98 99 bibi12d J=NNzaωNIENzaωNJif-J=NaIEzaIEaJNzaωNIENzaωNNaIEz
101 100 adantr J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-J=NaIEzaIEaJNzaωNIENzaωNNaIEz
102 97 101 mpbird J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-J=NaIEzaIEaJ
103 94 adantl ¬J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNI=aI
104 72 adantrl ¬J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNJ=aJ
105 103 104 breq12d ¬J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJaIEaJ
106 ifpfal ¬J=Nif-J=NaIEzaIEaJaIEaJ
107 106 bicomd ¬J=NaIEaJif-J=NaIEzaIEaJ
108 107 adantr ¬J=N¬I=NNωIωJωaMωzMNzaωNMωaIEaJif-J=NaIEzaIEaJ
109 105 108 bitrd ¬J=N¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-J=NaIEzaIEaJ
110 102 109 pm2.61ian ¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-J=NaIEzaIEaJ
111 ifpfal ¬I=Nif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJif-J=NaIEzaIEaJ
112 111 bicomd ¬I=Nif-J=NaIEzaIEaJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
113 112 adantr ¬I=NNωIωJωaMωzMNzaωNMωif-J=NaIEzaIEaJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
114 110 113 bitrd ¬I=NNωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
115 85 114 pm2.61ian NωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
116 48 115 bitrd NωIωJωaMωzMNzaωNMωNzaωNMωNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
117 45 116 mpdan NωIωJωaMωzMNzaωNMωNzaωNIENzaωNJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
118 5 117 bitrd NωIωJωaMωzMNzaωNbMω|bIEbJif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
119 118 ralbidva NωIωJωaMωzMNzaωNbMω|bIEbJzMif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ
120 119 rabbidva NωIωJωaMω|zMNzaωNbMω|bIEbJ=aMω|zMif-I=Nif-J=NzEzzEaJif-J=NaIEzaIEaJ