Metamath Proof Explorer

Theorem fmla1

Description: The valid Godel formulas of height 1 is the set of all formulas of the form ( a |g b ) and A.g k a with atoms a , b of the form x e. y . (Contributed by AV, 20-Sep-2023)

Ref Expression
Assertion fmla1 
|- ( Fmla ` 1o ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) } )

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 fveq2i 
 |-  ( Fmla ` 1o ) = ( Fmla ` suc (/) )
3 peano1 
 |-  (/) e. _om
4 fmlasuc 
 |-  ( (/) e. _om -> ( Fmla ` suc (/) ) = ( ( Fmla ` (/) ) u. { x | E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) } ) )
5 3 4 ax-mp 
 |-  ( Fmla ` suc (/) ) = ( ( Fmla ` (/) ) u. { x | E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) } )
6 fmla0xp 
 |-  ( Fmla ` (/) ) = ( { (/) } X. ( _om X. _om ) )
7 fmla0 
 |-  ( Fmla ` (/) ) = { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) }
8 7 rexeqi 
 |-  ( E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) <-> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) )
9 eqeq1 
 |-  ( y = p -> ( y = ( i e.g j ) <-> p = ( i e.g j ) ) )
10 9 2rexbidv 
 |-  ( y = p -> ( E. i e. _om E. j e. _om y = ( i e.g j ) <-> E. i e. _om E. j e. _om p = ( i e.g j ) ) )
11 10 elrab 
 |-  ( p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } <-> ( p e. _V /\ E. i e. _om E. j e. _om p = ( i e.g j ) ) )
12 oveq1 
 |-  ( p = ( i e.g j ) -> ( p |g q ) = ( ( i e.g j ) |g q ) )
13 12 eqeq2d 
 |-  ( p = ( i e.g j ) -> ( x = ( p |g q ) <-> x = ( ( i e.g j ) |g q ) ) )
14 13 rexbidv 
 |-  ( p = ( i e.g j ) -> ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) <-> E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) |g q ) ) )
15 eqidd 
 |-  ( p = ( i e.g j ) -> k = k )
16 id 
 |-  ( p = ( i e.g j ) -> p = ( i e.g j ) )
17 15 16 goaleq12d 
 |-  ( p = ( i e.g j ) -> A.g k p = A.g k ( i e.g j ) )
18 17 eqeq2d 
 |-  ( p = ( i e.g j ) -> ( x = A.g k p <-> x = A.g k ( i e.g j ) ) )
19 18 rexbidv 
 |-  ( p = ( i e.g j ) -> ( E. k e. _om x = A.g k p <-> E. k e. _om x = A.g k ( i e.g j ) ) )
20 14 19 orbi12d 
 |-  ( p = ( i e.g j ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) <-> ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) |g q ) \/ E. k e. _om x = A.g k ( i e.g j ) ) ) )
21 eqeq1 
 |-  ( z = q -> ( z = ( k e.g l ) <-> q = ( k e.g l ) ) )
22 21 2rexbidv 
 |-  ( z = q -> ( E. k e. _om E. l e. _om z = ( k e.g l ) <-> E. k e. _om E. l e. _om q = ( k e.g l ) ) )
23 fmla0 
 |-  ( Fmla ` (/) ) = { z e. _V | E. k e. _om E. l e. _om z = ( k e.g l ) }
24 22 23 elrab2 
 |-  ( q e. ( Fmla ` (/) ) <-> ( q e. _V /\ E. k e. _om E. l e. _om q = ( k e.g l ) ) )
25 oveq2 
 |-  ( q = ( k e.g l ) -> ( ( i e.g j ) |g q ) = ( ( i e.g j ) |g ( k e.g l ) ) )
26 25 eqeq2d 
 |-  ( q = ( k e.g l ) -> ( x = ( ( i e.g j ) |g q ) <-> x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
27 26 biimpcd 
 |-  ( x = ( ( i e.g j ) |g q ) -> ( q = ( k e.g l ) -> x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
28 27 reximdv 
 |-  ( x = ( ( i e.g j ) |g q ) -> ( E. l e. _om q = ( k e.g l ) -> E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
29 28 reximdv 
 |-  ( x = ( ( i e.g j ) |g q ) -> ( E. k e. _om E. l e. _om q = ( k e.g l ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
30 29 com12 
 |-  ( E. k e. _om E. l e. _om q = ( k e.g l ) -> ( x = ( ( i e.g j ) |g q ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
31 24 30 simplbiim 
 |-  ( q e. ( Fmla ` (/) ) -> ( x = ( ( i e.g j ) |g q ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
32 31 rexlimiv 
 |-  ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) |g q ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) )
33 32 orim1i 
 |-  ( ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) |g q ) \/ E. k e. _om x = A.g k ( i e.g j ) ) -> ( E. k e. _om E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ E. k e. _om x = A.g k ( i e.g j ) ) )
34 r19.43 
 |-  ( E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> ( E. k e. _om E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ E. k e. _om x = A.g k ( i e.g j ) ) )
35 33 34 sylibr 
 |-  ( ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) |g q ) \/ E. k e. _om x = A.g k ( i e.g j ) ) -> E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
36 20 35 syl6bi 
 |-  ( p = ( i e.g j ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
37 36 com12 
 |-  ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> ( p = ( i e.g j ) -> E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
38 37 reximdv 
 |-  ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> ( E. j e. _om p = ( i e.g j ) -> E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
39 38 reximdv 
 |-  ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> ( E. i e. _om E. j e. _om p = ( i e.g j ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
40 39 com12 
 |-  ( E. i e. _om E. j e. _om p = ( i e.g j ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
41 11 40 simplbiim 
 |-  ( p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } -> ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
42 41 rexlimiv 
 |-  ( E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
43 oveq1 
 |-  ( i = m -> ( i e.g j ) = ( m e.g j ) )
44 43 oveq1d 
 |-  ( i = m -> ( ( i e.g j ) |g ( k e.g l ) ) = ( ( m e.g j ) |g ( k e.g l ) ) )
45 44 eqeq2d 
 |-  ( i = m -> ( x = ( ( i e.g j ) |g ( k e.g l ) ) <-> x = ( ( m e.g j ) |g ( k e.g l ) ) ) )
46 45 rexbidv 
 |-  ( i = m -> ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) <-> E. l e. _om x = ( ( m e.g j ) |g ( k e.g l ) ) ) )
47 eqidd 
 |-  ( i = m -> k = k )
48 47 43 goaleq12d 
 |-  ( i = m -> A.g k ( i e.g j ) = A.g k ( m e.g j ) )
49 48 eqeq2d 
 |-  ( i = m -> ( x = A.g k ( i e.g j ) <-> x = A.g k ( m e.g j ) ) )
50 46 49 orbi12d 
 |-  ( i = m -> ( ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> ( E. l e. _om x = ( ( m e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) ) )
51 50 rexbidv 
 |-  ( i = m -> ( E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> E. k e. _om ( E. l e. _om x = ( ( m e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) ) )
52 oveq2 
 |-  ( j = n -> ( m e.g j ) = ( m e.g n ) )
53 52 oveq1d 
 |-  ( j = n -> ( ( m e.g j ) |g ( k e.g l ) ) = ( ( m e.g n ) |g ( k e.g l ) ) )
54 53 eqeq2d 
 |-  ( j = n -> ( x = ( ( m e.g j ) |g ( k e.g l ) ) <-> x = ( ( m e.g n ) |g ( k e.g l ) ) ) )
55 54 rexbidv 
 |-  ( j = n -> ( E. l e. _om x = ( ( m e.g j ) |g ( k e.g l ) ) <-> E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) ) )
56 eqidd 
 |-  ( j = n -> k = k )
57 56 52 goaleq12d 
 |-  ( j = n -> A.g k ( m e.g j ) = A.g k ( m e.g n ) )
58 57 eqeq2d 
 |-  ( j = n -> ( x = A.g k ( m e.g j ) <-> x = A.g k ( m e.g n ) ) )
59 55 58 orbi12d 
 |-  ( j = n -> ( ( E. l e. _om x = ( ( m e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) <-> ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) ) )
60 59 rexbidv 
 |-  ( j = n -> ( E. k e. _om ( E. l e. _om x = ( ( m e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) <-> E. k e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) ) )
61 51 60 cbvrex2vw 
 |-  ( E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> E. m e. _om E. n e. _om E. k e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) )
62 oveq1 
 |-  ( k = o -> ( k e.g l ) = ( o e.g l ) )
63 62 oveq2d 
 |-  ( k = o -> ( ( m e.g n ) |g ( k e.g l ) ) = ( ( m e.g n ) |g ( o e.g l ) ) )
64 63 eqeq2d 
 |-  ( k = o -> ( x = ( ( m e.g n ) |g ( k e.g l ) ) <-> x = ( ( m e.g n ) |g ( o e.g l ) ) ) )
65 64 rexbidv 
 |-  ( k = o -> ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) <-> E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) ) )
66 id 
 |-  ( k = o -> k = o )
67 eqidd 
 |-  ( k = o -> ( m e.g n ) = ( m e.g n ) )
68 66 67 goaleq12d 
 |-  ( k = o -> A.g k ( m e.g n ) = A.g o ( m e.g n ) )
69 68 eqeq2d 
 |-  ( k = o -> ( x = A.g k ( m e.g n ) <-> x = A.g o ( m e.g n ) ) )
70 65 69 orbi12d 
 |-  ( k = o -> ( ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) <-> ( E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) )
71 70 cbvrexvw 
 |-  ( E. k e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) <-> E. o e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) )
72 3 ne0ii 
 |-  _om =/= (/)
73 r19.44zv 
 |-  ( _om =/= (/) -> ( E. l e. _om ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) <-> ( E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) )
74 72 73 ax-mp 
 |-  ( E. l e. _om ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) <-> ( E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) )
75 eqeq1 
 |-  ( y = ( m e.g n ) -> ( y = ( i e.g j ) <-> ( m e.g n ) = ( i e.g j ) ) )
76 75 2rexbidv 
 |-  ( y = ( m e.g n ) -> ( E. i e. _om E. j e. _om y = ( i e.g j ) <-> E. i e. _om E. j e. _om ( m e.g n ) = ( i e.g j ) ) )
77 ovexd 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> ( m e.g n ) e. _V )
78 simpl 
 |-  ( ( m e. _om /\ n e. _om ) -> m e. _om )
79 43 eqeq2d 
 |-  ( i = m -> ( ( m e.g n ) = ( i e.g j ) <-> ( m e.g n ) = ( m e.g j ) ) )
80 79 rexbidv 
 |-  ( i = m -> ( E. j e. _om ( m e.g n ) = ( i e.g j ) <-> E. j e. _om ( m e.g n ) = ( m e.g j ) ) )
81 80 adantl 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ i = m ) -> ( E. j e. _om ( m e.g n ) = ( i e.g j ) <-> E. j e. _om ( m e.g n ) = ( m e.g j ) ) )
82 simpr 
 |-  ( ( m e. _om /\ n e. _om ) -> n e. _om )
83 52 eqeq2d 
 |-  ( j = n -> ( ( m e.g n ) = ( m e.g j ) <-> ( m e.g n ) = ( m e.g n ) ) )
84 83 adantl 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ j = n ) -> ( ( m e.g n ) = ( m e.g j ) <-> ( m e.g n ) = ( m e.g n ) ) )
85 eqidd 
 |-  ( ( m e. _om /\ n e. _om ) -> ( m e.g n ) = ( m e.g n ) )
86 82 84 85 rspcedvd 
 |-  ( ( m e. _om /\ n e. _om ) -> E. j e. _om ( m e.g n ) = ( m e.g j ) )
87 78 81 86 rspcedvd 
 |-  ( ( m e. _om /\ n e. _om ) -> E. i e. _om E. j e. _om ( m e.g n ) = ( i e.g j ) )
88 87 ad5ant12 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> E. i e. _om E. j e. _om ( m e.g n ) = ( i e.g j ) )
89 76 77 88 elrabd 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> ( m e.g n ) e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } )
90 oveq1 
 |-  ( p = ( m e.g n ) -> ( p |g q ) = ( ( m e.g n ) |g q ) )
91 90 eqeq2d 
 |-  ( p = ( m e.g n ) -> ( x = ( p |g q ) <-> x = ( ( m e.g n ) |g q ) ) )
92 91 rexbidv 
 |-  ( p = ( m e.g n ) -> ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) <-> E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) ) )
93 eqidd 
 |-  ( p = ( m e.g n ) -> k = k )
94 id 
 |-  ( p = ( m e.g n ) -> p = ( m e.g n ) )
95 93 94 goaleq12d 
 |-  ( p = ( m e.g n ) -> A.g k p = A.g k ( m e.g n ) )
96 95 eqeq2d 
 |-  ( p = ( m e.g n ) -> ( x = A.g k p <-> x = A.g k ( m e.g n ) ) )
97 96 rexbidv 
 |-  ( p = ( m e.g n ) -> ( E. k e. _om x = A.g k p <-> E. k e. _om x = A.g k ( m e.g n ) ) )
98 92 97 orbi12d 
 |-  ( p = ( m e.g n ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) <-> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) ) )
99 98 adantl 
 |-  ( ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) /\ p = ( m e.g n ) ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) <-> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) ) )
100 ovexd 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( o e.g l ) e. _V )
101 simpr 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) -> o e. _om )
102 101 adantr 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> o e. _om )
103 oveq1 
 |-  ( i = o -> ( i e.g j ) = ( o e.g j ) )
104 103 eqeq2d 
 |-  ( i = o -> ( ( o e.g l ) = ( i e.g j ) <-> ( o e.g l ) = ( o e.g j ) ) )
105 104 rexbidv 
 |-  ( i = o -> ( E. j e. _om ( o e.g l ) = ( i e.g j ) <-> E. j e. _om ( o e.g l ) = ( o e.g j ) ) )
106 105 adantl 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ i = o ) -> ( E. j e. _om ( o e.g l ) = ( i e.g j ) <-> E. j e. _om ( o e.g l ) = ( o e.g j ) ) )
107 simpr 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> l e. _om )
108 oveq2 
 |-  ( j = l -> ( o e.g j ) = ( o e.g l ) )
109 108 eqeq2d 
 |-  ( j = l -> ( ( o e.g l ) = ( o e.g j ) <-> ( o e.g l ) = ( o e.g l ) ) )
110 109 adantl 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ j = l ) -> ( ( o e.g l ) = ( o e.g j ) <-> ( o e.g l ) = ( o e.g l ) ) )
111 eqidd 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( o e.g l ) = ( o e.g l ) )
112 107 110 111 rspcedvd 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> E. j e. _om ( o e.g l ) = ( o e.g j ) )
113 102 106 112 rspcedvd 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> E. i e. _om E. j e. _om ( o e.g l ) = ( i e.g j ) )
114 eqeq1 
 |-  ( p = ( o e.g l ) -> ( p = ( i e.g j ) <-> ( o e.g l ) = ( i e.g j ) ) )
115 114 2rexbidv 
 |-  ( p = ( o e.g l ) -> ( E. i e. _om E. j e. _om p = ( i e.g j ) <-> E. i e. _om E. j e. _om ( o e.g l ) = ( i e.g j ) ) )
116 fmla0 
 |-  ( Fmla ` (/) ) = { p e. _V | E. i e. _om E. j e. _om p = ( i e.g j ) }
117 115 116 elrab2 
 |-  ( ( o e.g l ) e. ( Fmla ` (/) ) <-> ( ( o e.g l ) e. _V /\ E. i e. _om E. j e. _om ( o e.g l ) = ( i e.g j ) ) )
118 100 113 117 sylanbrc 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( o e.g l ) e. ( Fmla ` (/) ) )
119 118 adantr 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) |g ( o e.g l ) ) ) -> ( o e.g l ) e. ( Fmla ` (/) ) )
120 oveq2 
 |-  ( q = ( o e.g l ) -> ( ( m e.g n ) |g q ) = ( ( m e.g n ) |g ( o e.g l ) ) )
121 120 eqeq2d 
 |-  ( q = ( o e.g l ) -> ( x = ( ( m e.g n ) |g q ) <-> x = ( ( m e.g n ) |g ( o e.g l ) ) ) )
122 121 adantl 
 |-  ( ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) |g ( o e.g l ) ) ) /\ q = ( o e.g l ) ) -> ( x = ( ( m e.g n ) |g q ) <-> x = ( ( m e.g n ) |g ( o e.g l ) ) ) )
123 simpr 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) |g ( o e.g l ) ) ) -> x = ( ( m e.g n ) |g ( o e.g l ) ) )
124 119 122 123 rspcedvd 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) |g ( o e.g l ) ) ) -> E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) )
125 124 ex 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( x = ( ( m e.g n ) |g ( o e.g l ) ) -> E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) ) )
126 102 adantr 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) -> o e. _om )
127 69 adantl 
 |-  ( ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) /\ k = o ) -> ( x = A.g k ( m e.g n ) <-> x = A.g o ( m e.g n ) ) )
128 simpr 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) -> x = A.g o ( m e.g n ) )
129 126 127 128 rspcedvd 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) -> E. k e. _om x = A.g k ( m e.g n ) )
130 129 ex 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( x = A.g o ( m e.g n ) -> E. k e. _om x = A.g k ( m e.g n ) ) )
131 125 130 orim12d 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) ) )
132 131 imp 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) |g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) )
133 89 99 132 rspcedvd 
 |-  ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) )
134 133 ex 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) ) )
135 134 rexlimdva 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) -> ( E. l e. _om ( x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) ) )
136 74 135 syl5bir 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) -> ( ( E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) ) )
137 136 rexlimdva 
 |-  ( ( m e. _om /\ n e. _om ) -> ( E. o e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) ) )
138 71 137 syl5bi 
 |-  ( ( m e. _om /\ n e. _om ) -> ( E. k e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) ) )
139 138 rexlimivv 
 |-  ( E. m e. _om E. n e. _om E. k e. _om ( E. l e. _om x = ( ( m e.g n ) |g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) )
140 61 139 sylbi 
 |-  ( E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) -> E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) )
141 42 140 impbii 
 |-  ( E. p e. { y e. _V | E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) <-> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
142 8 141 bitri 
 |-  ( E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) <-> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
143 142 abbii 
 |-  { x | E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) } = { x | E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) }
144 6 143 uneq12i 
 |-  ( ( Fmla ` (/) ) u. { x | E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p |g q ) \/ E. k e. _om x = A.g k p ) } ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) } )
145 2 5 144 3eqtri 
 |-  ( Fmla ` 1o ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) |g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) } )