Metamath Proof Explorer

Theorem fimgmcyclem

Description: Lemma for fimgmcyc . (Contributed by SN, 7-Jul-2025)

Ref Expression
Hypothesis fimgmcyclem.s 
|- ( ph -> E. o e. NN E. q e. NN ( o =/= q /\ ( o .x. A ) = ( q .x. A ) ) )
Assertion fimgmcyclem 
|- ( ph -> E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) )

Proof

Step Hyp Ref Expression
1 fimgmcyclem.s 
 |-  ( ph -> E. o e. NN E. q e. NN ( o =/= q /\ ( o .x. A ) = ( q .x. A ) ) )
2 simpr 
 |-  ( ( ph /\ E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) ) -> E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) )
3 rexcom 
 |-  ( E. r e. NN E. p e. NN ( p < r /\ ( r .x. A ) = ( p .x. A ) ) <-> E. p e. NN E. r e. NN ( p < r /\ ( r .x. A ) = ( p .x. A ) ) )
4 eqcom 
 |-  ( ( r .x. A ) = ( p .x. A ) <-> ( p .x. A ) = ( r .x. A ) )
5 4 anbi2i 
 |-  ( ( p < r /\ ( r .x. A ) = ( p .x. A ) ) <-> ( p < r /\ ( p .x. A ) = ( r .x. A ) ) )
6 5 2rexbii 
 |-  ( E. p e. NN E. r e. NN ( p < r /\ ( r .x. A ) = ( p .x. A ) ) <-> E. p e. NN E. r e. NN ( p < r /\ ( p .x. A ) = ( r .x. A ) ) )
7 3 6 sylbb 
 |-  ( E. r e. NN E. p e. NN ( p < r /\ ( r .x. A ) = ( p .x. A ) ) -> E. p e. NN E. r e. NN ( p < r /\ ( p .x. A ) = ( r .x. A ) ) )
8 breq2 
 |-  ( o = r -> ( p < o <-> p < r ) )
9 oveq1 
 |-  ( o = r -> ( o .x. A ) = ( r .x. A ) )
10 9 eqeq1d 
 |-  ( o = r -> ( ( o .x. A ) = ( p .x. A ) <-> ( r .x. A ) = ( p .x. A ) ) )
11 8 10 anbi12d 
 |-  ( o = r -> ( ( p < o /\ ( o .x. A ) = ( p .x. A ) ) <-> ( p < r /\ ( r .x. A ) = ( p .x. A ) ) ) )
12 11 rexbidv 
 |-  ( o = r -> ( E. p e. NN ( p < o /\ ( o .x. A ) = ( p .x. A ) ) <-> E. p e. NN ( p < r /\ ( r .x. A ) = ( p .x. A ) ) ) )
13 12 cbvrexvw 
 |-  ( E. o e. NN E. p e. NN ( p < o /\ ( o .x. A ) = ( p .x. A ) ) <-> E. r e. NN E. p e. NN ( p < r /\ ( r .x. A ) = ( p .x. A ) ) )
14 breq1 
 |-  ( o = p -> ( o < r <-> p < r ) )
15 oveq1 
 |-  ( o = p -> ( o .x. A ) = ( p .x. A ) )
16 15 eqeq1d 
 |-  ( o = p -> ( ( o .x. A ) = ( r .x. A ) <-> ( p .x. A ) = ( r .x. A ) ) )
17 14 16 anbi12d 
 |-  ( o = p -> ( ( o < r /\ ( o .x. A ) = ( r .x. A ) ) <-> ( p < r /\ ( p .x. A ) = ( r .x. A ) ) ) )
18 17 rexbidv 
 |-  ( o = p -> ( E. r e. NN ( o < r /\ ( o .x. A ) = ( r .x. A ) ) <-> E. r e. NN ( p < r /\ ( p .x. A ) = ( r .x. A ) ) ) )
19 18 cbvrexvw 
 |-  ( E. o e. NN E. r e. NN ( o < r /\ ( o .x. A ) = ( r .x. A ) ) <-> E. p e. NN E. r e. NN ( p < r /\ ( p .x. A ) = ( r .x. A ) ) )
20 7 13 19 3imtr4i 
 |-  ( E. o e. NN E. p e. NN ( p < o /\ ( o .x. A ) = ( p .x. A ) ) -> E. o e. NN E. r e. NN ( o < r /\ ( o .x. A ) = ( r .x. A ) ) )
21 breq1 
 |-  ( q = p -> ( q < o <-> p < o ) )
22 oveq1 
 |-  ( q = p -> ( q .x. A ) = ( p .x. A ) )
23 22 eqeq2d 
 |-  ( q = p -> ( ( o .x. A ) = ( q .x. A ) <-> ( o .x. A ) = ( p .x. A ) ) )
24 21 23 anbi12d 
 |-  ( q = p -> ( ( q < o /\ ( o .x. A ) = ( q .x. A ) ) <-> ( p < o /\ ( o .x. A ) = ( p .x. A ) ) ) )
25 24 cbvrexvw 
 |-  ( E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) <-> E. p e. NN ( p < o /\ ( o .x. A ) = ( p .x. A ) ) )
26 25 rexbii 
 |-  ( E. o e. NN E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) <-> E. o e. NN E. p e. NN ( p < o /\ ( o .x. A ) = ( p .x. A ) ) )
27 breq2 
 |-  ( q = r -> ( o < q <-> o < r ) )
28 oveq1 
 |-  ( q = r -> ( q .x. A ) = ( r .x. A ) )
29 28 eqeq2d 
 |-  ( q = r -> ( ( o .x. A ) = ( q .x. A ) <-> ( o .x. A ) = ( r .x. A ) ) )
30 27 29 anbi12d 
 |-  ( q = r -> ( ( o < q /\ ( o .x. A ) = ( q .x. A ) ) <-> ( o < r /\ ( o .x. A ) = ( r .x. A ) ) ) )
31 30 cbvrexvw 
 |-  ( E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) <-> E. r e. NN ( o < r /\ ( o .x. A ) = ( r .x. A ) ) )
32 31 rexbii 
 |-  ( E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) <-> E. o e. NN E. r e. NN ( o < r /\ ( o .x. A ) = ( r .x. A ) ) )
33 20 26 32 3imtr4i 
 |-  ( E. o e. NN E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) -> E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) )
34 33 adantl 
 |-  ( ( ph /\ E. o e. NN E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) -> E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) )
35 simpl 
 |-  ( ( o e. NN /\ q e. NN ) -> o e. NN )
36 35 nnred 
 |-  ( ( o e. NN /\ q e. NN ) -> o e. RR )
37 simpr 
 |-  ( ( o e. NN /\ q e. NN ) -> q e. NN )
38 37 nnred 
 |-  ( ( o e. NN /\ q e. NN ) -> q e. RR )
39 36 38 lttri2d 
 |-  ( ( o e. NN /\ q e. NN ) -> ( o =/= q <-> ( o < q \/ q < o ) ) )
40 39 anbi1d 
 |-  ( ( o e. NN /\ q e. NN ) -> ( ( o =/= q /\ ( o .x. A ) = ( q .x. A ) ) <-> ( ( o < q \/ q < o ) /\ ( o .x. A ) = ( q .x. A ) ) ) )
41 andir 
 |-  ( ( ( o < q \/ q < o ) /\ ( o .x. A ) = ( q .x. A ) ) <-> ( ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
42 40 41 bitrdi 
 |-  ( ( o e. NN /\ q e. NN ) -> ( ( o =/= q /\ ( o .x. A ) = ( q .x. A ) ) <-> ( ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) ) )
43 42 2rexbiia 
 |-  ( E. o e. NN E. q e. NN ( o =/= q /\ ( o .x. A ) = ( q .x. A ) ) <-> E. o e. NN E. q e. NN ( ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
44 r19.43 
 |-  ( E. q e. NN ( ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) <-> ( E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
45 44 rexbii 
 |-  ( E. o e. NN E. q e. NN ( ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) <-> E. o e. NN ( E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
46 r19.43 
 |-  ( E. o e. NN ( E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) <-> ( E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ E. o e. NN E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
47 43 45 46 3bitri 
 |-  ( E. o e. NN E. q e. NN ( o =/= q /\ ( o .x. A ) = ( q .x. A ) ) <-> ( E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ E. o e. NN E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
48 1 47 sylib 
 |-  ( ph -> ( E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) \/ E. o e. NN E. q e. NN ( q < o /\ ( o .x. A ) = ( q .x. A ) ) ) )
49 2 34 48 mpjaodan 
 |-  ( ph -> E. o e. NN E. q e. NN ( o < q /\ ( o .x. A ) = ( q .x. A ) ) )