Metamath Proof Explorer

Theorem satfv1lem

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

Ref Expression
Assertion satfv1lem 
|- ( ( N e. _om /\ I e. _om /\ J e. _om ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. { b e. ( M ^m _om ) | ( b ` I ) E ( b ` J ) } } = { a e. ( M ^m _om ) | A. z e. 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 fveq1 
 |-  ( b = ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) -> ( b ` I ) = ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) )
2 fveq1 
 |-  ( b = ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) -> ( b ` J ) = ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) )
3 1 2 breq12d 
 |-  ( b = ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) -> ( ( b ` I ) E ( b ` J ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) )
4 3 elrab 
 |-  ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. { b e. ( M ^m _om ) | ( b ` I ) E ( b ` J ) } <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) )
5 4 a1i 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. { b e. ( M ^m _om ) | ( b ` I ) E ( b ` J ) } <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) ) )
6 elex 
 |-  ( N e. _om -> N e. _V )
7 6 3ad2ant1 
 |-  ( ( N e. _om /\ I e. _om /\ J e. _om ) -> N e. _V )
8 7 ad2antrr 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> N e. _V )
9 simpr 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> z e. M )
10 8 9 fsnd 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> { <. N , z >. } : { N } --> M )
11 elmapex 
 |-  ( a e. ( M ^m _om ) -> ( M e. _V /\ _om e. _V ) )
12 11 simpld 
 |-  ( a e. ( M ^m _om ) -> M e. _V )
13 12 adantr 
 |-  ( ( a e. ( M ^m _om ) /\ z e. M ) -> M e. _V )
14 snex 
 |-  { N } e. _V
15 14 a1i 
 |-  ( ( a e. ( M ^m _om ) /\ z e. M ) -> { N } e. _V )
16 13 15 elmapd 
 |-  ( ( a e. ( M ^m _om ) /\ z e. M ) -> ( { <. N , z >. } e. ( M ^m { N } ) <-> { <. N , z >. } : { N } --> M ) )
17 16 adantll 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( { <. N , z >. } e. ( M ^m { N } ) <-> { <. N , z >. } : { N } --> M ) )
18 10 17 mpbird 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> { <. N , z >. } e. ( M ^m { N } ) )
19 elmapi 
 |-  ( a e. ( M ^m _om ) -> a : _om --> M )
20 difssd 
 |-  ( a e. ( M ^m _om ) -> ( _om \ { N } ) C_ _om )
21 19 20 fssresd 
 |-  ( a e. ( M ^m _om ) -> ( a |` ( _om \ { N } ) ) : ( _om \ { N } ) --> M )
22 omex 
 |-  _om e. _V
23 22 difexi 
 |-  ( _om \ { N } ) e. _V
24 23 a1i 
 |-  ( a e. ( M ^m _om ) -> ( _om \ { N } ) e. _V )
25 12 24 elmapd 
 |-  ( a e. ( M ^m _om ) -> ( ( a |` ( _om \ { N } ) ) e. ( M ^m ( _om \ { N } ) ) <-> ( a |` ( _om \ { N } ) ) : ( _om \ { N } ) --> M ) )
26 21 25 mpbird 
 |-  ( a e. ( M ^m _om ) -> ( a |` ( _om \ { N } ) ) e. ( M ^m ( _om \ { N } ) ) )
27 26 adantl 
 |-  ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) -> ( a |` ( _om \ { N } ) ) e. ( M ^m ( _om \ { N } ) ) )
28 27 adantr 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( a |` ( _om \ { N } ) ) e. ( M ^m ( _om \ { N } ) ) )
29 res0 
 |-  ( { <. N , z >. } |` (/) ) = (/)
30 res0 
 |-  ( ( a |` ( _om \ { N } ) ) |` (/) ) = (/)
31 29 30 eqtr4i 
 |-  ( { <. N , z >. } |` (/) ) = ( ( a |` ( _om \ { N } ) ) |` (/) )
32 disjdif 
 |-  ( { N } i^i ( _om \ { N } ) ) = (/)
33 32 reseq2i 
 |-  ( { <. N , z >. } |` ( { N } i^i ( _om \ { N } ) ) ) = ( { <. N , z >. } |` (/) )
34 32 reseq2i 
 |-  ( ( a |` ( _om \ { N } ) ) |` ( { N } i^i ( _om \ { N } ) ) ) = ( ( a |` ( _om \ { N } ) ) |` (/) )
35 31 33 34 3eqtr4i 
 |-  ( { <. N , z >. } |` ( { N } i^i ( _om \ { N } ) ) ) = ( ( a |` ( _om \ { N } ) ) |` ( { N } i^i ( _om \ { N } ) ) )
36 35 a1i 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( { <. N , z >. } |` ( { N } i^i ( _om \ { N } ) ) ) = ( ( a |` ( _om \ { N } ) ) |` ( { N } i^i ( _om \ { N } ) ) ) )
37 elmapresaun 
 |-  ( ( { <. N , z >. } e. ( M ^m { N } ) /\ ( a |` ( _om \ { N } ) ) e. ( M ^m ( _om \ { N } ) ) /\ ( { <. N , z >. } |` ( { N } i^i ( _om \ { N } ) ) ) = ( ( a |` ( _om \ { N } ) ) |` ( { N } i^i ( _om \ { N } ) ) ) ) -> ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m ( { N } u. ( _om \ { N } ) ) ) )
38 18 28 36 37 syl3anc 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m ( { N } u. ( _om \ { N } ) ) ) )
39 uncom 
 |-  ( { N } u. ( _om \ { N } ) ) = ( ( _om \ { N } ) u. { N } )
40 difsnid 
 |-  ( N e. _om -> ( ( _om \ { N } ) u. { N } ) = _om )
41 39 40 syl5req 
 |-  ( N e. _om -> _om = ( { N } u. ( _om \ { N } ) ) )
42 41 3ad2ant1 
 |-  ( ( N e. _om /\ I e. _om /\ J e. _om ) -> _om = ( { N } u. ( _om \ { N } ) ) )
43 42 ad2antrr 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> _om = ( { N } u. ( _om \ { N } ) ) )
44 43 oveq2d 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( M ^m _om ) = ( M ^m ( { N } u. ( _om \ { N } ) ) ) )
45 38 44 eleqtrrd 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) )
46 ibar 
 |-  ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) ) )
47 46 adantl 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) ) )
48 47 bicomd 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) )
49 simpll1 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> N e. _om )
50 eqid 
 |-  ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) = ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) )
51 49 9 50 fvsnun1 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) = z )
52 51 adantr 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) = z )
53 52 52 breq12d 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> z E z ) )
54 53 adantl 
 |-  ( ( J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> z E z ) )
55 fveq2 
 |-  ( J = N -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) = ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) )
56 55 breq2d 
 |-  ( J = N -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) ) )
57 ifptru 
 |-  ( J = N -> ( if- ( J = N , z E z , z E ( a ` J ) ) <-> z E z ) )
58 56 57 bibi12d 
 |-  ( J = N -> ( ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) <-> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> z E z ) ) )
59 58 adantr 
 |-  ( ( J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) <-> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> z E z ) ) )
60 54 59 mpbird 
 |-  ( ( J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
61 52 adantl 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) = z )
62 49 adantr 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> N e. _om )
63 62 adantl 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> N e. _om )
64 9 adantr 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> z e. M )
65 64 adantl 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> z e. M )
66 neqne 
 |-  ( -. J = N -> J =/= N )
67 simpll3 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> J e. _om )
68 67 adantr 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> J e. _om )
69 66 68 anim12ci 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( J e. _om /\ J =/= N ) )
70 eldifsn 
 |-  ( J e. ( _om \ { N } ) <-> ( J e. _om /\ J =/= N ) )
71 69 70 sylibr 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> J e. ( _om \ { N } ) )
72 63 65 50 71 fvsnun2 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) = ( a ` J ) )
73 61 72 breq12d 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> z E ( a ` J ) ) )
74 ifpfal 
 |-  ( -. J = N -> ( if- ( J = N , z E z , z E ( a ` J ) ) <-> z E ( a ` J ) ) )
75 74 bicomd 
 |-  ( -. J = N -> ( z E ( a ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
76 75 adantr 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( z E ( a ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
77 73 76 bitrd 
 |-  ( ( -. J = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
78 60 77 pm2.61ian 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
79 78 adantl 
 |-  ( ( I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
80 fveq2 
 |-  ( I = N -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) = ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) )
81 80 breq1d 
 |-  ( I = N -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) )
82 ifptru 
 |-  ( I = N -> ( 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 ) ) ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) )
83 81 82 bibi12d 
 |-  ( I = N -> ( ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> 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 , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) ) )
84 83 adantr 
 |-  ( ( I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> 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 , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , z E z , z E ( a ` J ) ) ) ) )
85 79 84 mpbird 
 |-  ( ( I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> 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 ) ) ) ) )
86 62 adantl 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> N e. _om )
87 64 adantl 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> z e. M )
88 neqne 
 |-  ( -. I = N -> I =/= N )
89 simpll2 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> I e. _om )
90 89 adantr 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> I e. _om )
91 88 90 anim12ci 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( I e. _om /\ I =/= N ) )
92 eldifsn 
 |-  ( I e. ( _om \ { N } ) <-> ( I e. _om /\ I =/= N ) )
93 91 92 sylibr 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> I e. ( _om \ { N } ) )
94 86 87 50 93 fvsnun2 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) = ( a ` I ) )
95 52 adantl 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) = z )
96 94 95 breq12d 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> ( a ` I ) E z ) )
97 96 adantl 
 |-  ( ( J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> ( a ` I ) E z ) )
98 55 breq2d 
 |-  ( J = N -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) ) )
99 ifptru 
 |-  ( J = N -> ( if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) <-> ( a ` I ) E z ) )
100 98 99 bibi12d 
 |-  ( J = N -> ( ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) <-> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> ( a ` I ) E z ) ) )
101 100 adantr 
 |-  ( ( J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) <-> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` N ) <-> ( a ` I ) E z ) ) )
102 97 101 mpbird 
 |-  ( ( J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
103 94 adantl 
 |-  ( ( -. J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) = ( a ` I ) )
104 72 adantrl 
 |-  ( ( -. J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) = ( a ` J ) )
105 103 104 breq12d 
 |-  ( ( -. J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> ( a ` I ) E ( a ` J ) ) )
106 ifpfal 
 |-  ( -. J = N -> ( if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) <-> ( a ` I ) E ( a ` J ) ) )
107 106 bicomd 
 |-  ( -. J = N -> ( ( a ` I ) E ( a ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
108 107 adantr 
 |-  ( ( -. J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( a ` I ) E ( a ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
109 105 108 bitrd 
 |-  ( ( -. J = N /\ ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
110 102 109 pm2.61ian 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
111 ifpfal 
 |-  ( -. I = N -> ( 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 ) ) ) <-> if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
112 111 bicomd 
 |-  ( -. I = N -> ( if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) <-> 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 adantr 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( if- ( J = N , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) <-> 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 110 113 bitrd 
 |-  ( ( -. I = N /\ ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> 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 85 114 pm2.61ian 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) <-> 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 48 115 bitrd 
 |-  ( ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) /\ ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) <-> 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 45 116 mpdan 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. ( M ^m _om ) /\ ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` I ) E ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) ` J ) ) <-> 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 5 117 bitrd 
 |-  ( ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) /\ z e. M ) -> ( ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. { b e. ( M ^m _om ) | ( b ` I ) E ( b ` J ) } <-> 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 ralbidva 
 |-  ( ( ( N e. _om /\ I e. _om /\ J e. _om ) /\ a e. ( M ^m _om ) ) -> ( A. z e. M ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. { b e. ( M ^m _om ) | ( b ` I ) E ( b ` J ) } <-> A. z e. 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 119 rabbidva 
 |-  ( ( N e. _om /\ I e. _om /\ J e. _om ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. N , z >. } u. ( a |` ( _om \ { N } ) ) ) e. { b e. ( M ^m _om ) | ( b ` I ) E ( b ` J ) } } = { a e. ( M ^m _om ) | A. z e. 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 ) ) ) } )