Metamath Proof Explorer

Theorem ishlg2

Description: Alternate version of ishlg , including closure. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses ishlg.p 
|- P = ( Base ` G )
ishlg.i 
|- I = ( Itv ` G )
ishlg.k 
|- K = ( hlG ` G )
ishlg2.g 
|- ( ph -> G e. V )
ishlg2.1 
|- ( ph -> C e. P )
Assertion ishlg2 
|- ( ph -> ( A ( K ` C ) B <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishlg.p 
 |-  P = ( Base ` G )
2 ishlg.i 
 |-  I = ( Itv ` G )
3 ishlg.k 
 |-  K = ( hlG ` G )
4 ishlg2.g 
 |-  ( ph -> G e. V )
5 ishlg2.1 
 |-  ( ph -> C e. P )
6 neeq2 
 |-  ( c = C -> ( a =/= c <-> a =/= C ) )
7 neeq2 
 |-  ( c = C -> ( b =/= c <-> b =/= C ) )
8 oveq1 
 |-  ( c = C -> ( c I b ) = ( C I b ) )
9 8 eleq2d 
 |-  ( c = C -> ( a e. ( c I b ) <-> a e. ( C I b ) ) )
10 oveq1 
 |-  ( c = C -> ( c I a ) = ( C I a ) )
11 10 eleq2d 
 |-  ( c = C -> ( b e. ( c I a ) <-> b e. ( C I a ) ) )
12 9 11 orbi12d 
 |-  ( c = C -> ( ( a e. ( c I b ) \/ b e. ( c I a ) ) <-> ( a e. ( C I b ) \/ b e. ( C I a ) ) ) )
13 6 7 12 3anbi123d 
 |-  ( c = C -> ( ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) <-> ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) )
14 13 anbi2d 
 |-  ( c = C -> ( ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) <-> ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) ) )
15 14 opabbidv 
 |-  ( c = C -> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } )
16 elex 
 |-  ( G e. V -> G e. _V )
17 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
18 17 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
19 18 eleq2d 
 |-  ( g = G -> ( a e. ( Base ` g ) <-> a e. P ) )
20 18 eleq2d 
 |-  ( g = G -> ( b e. ( Base ` g ) <-> b e. P ) )
21 19 20 anbi12d 
 |-  ( g = G -> ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) <-> ( a e. P /\ b e. P ) ) )
22 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
23 22 2 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
24 23 oveqd 
 |-  ( g = G -> ( c ( Itv ` g ) b ) = ( c I b ) )
25 24 eleq2d 
 |-  ( g = G -> ( a e. ( c ( Itv ` g ) b ) <-> a e. ( c I b ) ) )
26 23 oveqd 
 |-  ( g = G -> ( c ( Itv ` g ) a ) = ( c I a ) )
27 26 eleq2d 
 |-  ( g = G -> ( b e. ( c ( Itv ` g ) a ) <-> b e. ( c I a ) ) )
28 25 27 orbi12d 
 |-  ( g = G -> ( ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) <-> ( a e. ( c I b ) \/ b e. ( c I a ) ) ) )
29 28 3anbi3d 
 |-  ( g = G -> ( ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) <-> ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) )
30 21 29 anbi12d 
 |-  ( g = G -> ( ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) <-> ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) ) )
31 30 opabbidv 
 |-  ( g = G -> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } )
32 18 31 mpteq12dv 
 |-  ( g = G -> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) } ) = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
33 df-hlg 
 |-  hlG = ( g e. _V |-> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) } ) )
34 32 33 1 mptfvmpt 
 |-  ( G e. _V -> ( hlG ` G ) = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
35 4 16 34 3syl 
 |-  ( ph -> ( hlG ` G ) = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
36 3 35 eqtrid 
 |-  ( ph -> K = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
37 1 fvexi 
 |-  P e. _V
38 37 37 xpex 
 |-  ( P X. P ) e. _V
39 opabssxp 
 |-  { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } C_ ( P X. P )
40 38 39 ssexi 
 |-  { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } e. _V
41 40 a1i 
 |-  ( ph -> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } e. _V )
42 15 36 5 41 fvmptd4 
 |-  ( ph -> ( K ` C ) = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } )
43 42 breqd 
 |-  ( ph -> ( A ( K ` C ) B <-> A { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } B ) )
44 simpl 
 |-  ( ( a = A /\ b = B ) -> a = A )
45 44 neeq1d 
 |-  ( ( a = A /\ b = B ) -> ( a =/= C <-> A =/= C ) )
46 simpr 
 |-  ( ( a = A /\ b = B ) -> b = B )
47 46 neeq1d 
 |-  ( ( a = A /\ b = B ) -> ( b =/= C <-> B =/= C ) )
48 46 oveq2d 
 |-  ( ( a = A /\ b = B ) -> ( C I b ) = ( C I B ) )
49 44 48 eleq12d 
 |-  ( ( a = A /\ b = B ) -> ( a e. ( C I b ) <-> A e. ( C I B ) ) )
50 44 oveq2d 
 |-  ( ( a = A /\ b = B ) -> ( C I a ) = ( C I A ) )
51 46 50 eleq12d 
 |-  ( ( a = A /\ b = B ) -> ( b e. ( C I a ) <-> B e. ( C I A ) ) )
52 49 51 orbi12d 
 |-  ( ( a = A /\ b = B ) -> ( ( a e. ( C I b ) \/ b e. ( C I a ) ) <-> ( A e. ( C I B ) \/ B e. ( C I A ) ) ) )
53 45 47 52 3anbi123d 
 |-  ( ( a = A /\ b = B ) -> ( ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
54 eqid 
 |-  { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) }
55 53 54 brab2a 
 |-  ( A { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } B <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
56 43 55 bitrdi 
 |-  ( ph -> ( A ( K ` C ) B <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) ) )