Step |
Hyp |
Ref |
Expression |
1 |
|
satfv1fvfmla1.x |
|- X = ( ( I e.g J ) |g ( K e.g L ) ) |
2 |
|
simpll |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> I e. _om ) |
3 |
|
simplr |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> J e. _om ) |
4 |
|
simprl |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> K e. _om ) |
5 |
|
simprr |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> L e. _om ) |
6 |
|
oveq2 |
|- ( n = L -> ( K e.g n ) = ( K e.g L ) ) |
7 |
6
|
oveq2d |
|- ( n = L -> ( ( I e.g J ) |g ( K e.g n ) ) = ( ( I e.g J ) |g ( K e.g L ) ) ) |
8 |
7
|
eqeq2d |
|- ( n = L -> ( X = ( ( I e.g J ) |g ( K e.g n ) ) <-> X = ( ( I e.g J ) |g ( K e.g L ) ) ) ) |
9 |
8
|
adantl |
|- ( ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) /\ n = L ) -> ( X = ( ( I e.g J ) |g ( K e.g n ) ) <-> X = ( ( I e.g J ) |g ( K e.g L ) ) ) ) |
10 |
1
|
a1i |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X = ( ( I e.g J ) |g ( K e.g L ) ) ) |
11 |
5 9 10
|
rspcedvd |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) ) |
12 |
11
|
orcd |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) \/ X = A.g K ( I e.g J ) ) ) |
13 |
|
oveq1 |
|- ( i = I -> ( i e.g j ) = ( I e.g j ) ) |
14 |
13
|
oveq1d |
|- ( i = I -> ( ( i e.g j ) |g ( k e.g n ) ) = ( ( I e.g j ) |g ( k e.g n ) ) ) |
15 |
14
|
eqeq2d |
|- ( i = I -> ( X = ( ( i e.g j ) |g ( k e.g n ) ) <-> X = ( ( I e.g j ) |g ( k e.g n ) ) ) ) |
16 |
15
|
rexbidv |
|- ( i = I -> ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) ) ) |
17 |
|
eqidd |
|- ( i = I -> k = k ) |
18 |
17 13
|
goaleq12d |
|- ( i = I -> A.g k ( i e.g j ) = A.g k ( I e.g j ) ) |
19 |
18
|
eqeq2d |
|- ( i = I -> ( X = A.g k ( i e.g j ) <-> X = A.g k ( I e.g j ) ) ) |
20 |
16 19
|
orbi12d |
|- ( i = I -> ( ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) <-> ( E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g j ) ) ) ) |
21 |
|
oveq2 |
|- ( j = J -> ( I e.g j ) = ( I e.g J ) ) |
22 |
21
|
oveq1d |
|- ( j = J -> ( ( I e.g j ) |g ( k e.g n ) ) = ( ( I e.g J ) |g ( k e.g n ) ) ) |
23 |
22
|
eqeq2d |
|- ( j = J -> ( X = ( ( I e.g j ) |g ( k e.g n ) ) <-> X = ( ( I e.g J ) |g ( k e.g n ) ) ) ) |
24 |
23
|
rexbidv |
|- ( j = J -> ( E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) ) ) |
25 |
|
eqidd |
|- ( j = J -> k = k ) |
26 |
25 21
|
goaleq12d |
|- ( j = J -> A.g k ( I e.g j ) = A.g k ( I e.g J ) ) |
27 |
26
|
eqeq2d |
|- ( j = J -> ( X = A.g k ( I e.g j ) <-> X = A.g k ( I e.g J ) ) ) |
28 |
24 27
|
orbi12d |
|- ( j = J -> ( ( E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g j ) ) <-> ( E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g J ) ) ) ) |
29 |
|
oveq1 |
|- ( k = K -> ( k e.g n ) = ( K e.g n ) ) |
30 |
29
|
oveq2d |
|- ( k = K -> ( ( I e.g J ) |g ( k e.g n ) ) = ( ( I e.g J ) |g ( K e.g n ) ) ) |
31 |
30
|
eqeq2d |
|- ( k = K -> ( X = ( ( I e.g J ) |g ( k e.g n ) ) <-> X = ( ( I e.g J ) |g ( K e.g n ) ) ) ) |
32 |
31
|
rexbidv |
|- ( k = K -> ( E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) ) ) |
33 |
|
id |
|- ( k = K -> k = K ) |
34 |
|
eqidd |
|- ( k = K -> ( I e.g J ) = ( I e.g J ) ) |
35 |
33 34
|
goaleq12d |
|- ( k = K -> A.g k ( I e.g J ) = A.g K ( I e.g J ) ) |
36 |
35
|
eqeq2d |
|- ( k = K -> ( X = A.g k ( I e.g J ) <-> X = A.g K ( I e.g J ) ) ) |
37 |
32 36
|
orbi12d |
|- ( k = K -> ( ( E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g J ) ) <-> ( E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) \/ X = A.g K ( I e.g J ) ) ) ) |
38 |
20 28 37
|
rspc3ev |
|- ( ( ( I e. _om /\ J e. _om /\ K e. _om ) /\ ( E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) \/ X = A.g K ( I e.g J ) ) ) -> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) |
39 |
2 3 4 12 38
|
syl31anc |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) |
40 |
1
|
ovexi |
|- X e. _V |
41 |
|
eqeq1 |
|- ( x = X -> ( x = ( ( i e.g j ) |g ( k e.g n ) ) <-> X = ( ( i e.g j ) |g ( k e.g n ) ) ) ) |
42 |
41
|
rexbidv |
|- ( x = X -> ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) ) ) |
43 |
|
eqeq1 |
|- ( x = X -> ( x = A.g k ( i e.g j ) <-> X = A.g k ( i e.g j ) ) ) |
44 |
42 43
|
orbi12d |
|- ( x = X -> ( ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) <-> ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) ) |
45 |
44
|
rexbidv |
|- ( x = X -> ( E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) <-> E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) ) |
46 |
45
|
2rexbidv |
|- ( x = X -> ( E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) <-> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) ) |
47 |
40 46
|
elab |
|- ( X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } <-> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) |
48 |
39 47
|
sylibr |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) |
49 |
48
|
olcd |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( X e. ( { (/) } X. ( _om X. _om ) ) \/ X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) ) |
50 |
|
elun |
|- ( X e. ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) <-> ( X e. ( { (/) } X. ( _om X. _om ) ) \/ X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) ) |
51 |
49 50
|
sylibr |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) ) |
52 |
|
fmla1 |
|- ( Fmla ` 1o ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) |
53 |
51 52
|
eleqtrrdi |
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. ( Fmla ` 1o ) ) |