Metamath Proof Explorer

Theorem lublecllem

Description: Lemma for lublecl and lubid . (Contributed by NM, 8-Sep-2018)

Ref Expression
Hypotheses lublecl.b 
|- B = ( Base ` K )
lublecl.l 
|- .<_ = ( le ` K )
lublecl.u 
|- U = ( lub ` K )
lublecl.k 
|- ( ph -> K e. Poset )
lublecl.x 
|- ( ph -> X e. B )
Assertion lublecllem 
|- ( ( ph /\ x e. B ) -> ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )

Proof

Step Hyp Ref Expression
1 lublecl.b 
 |-  B = ( Base ` K )
2 lublecl.l 
 |-  .<_ = ( le ` K )
3 lublecl.u 
 |-  U = ( lub ` K )
4 lublecl.k 
 |-  ( ph -> K e. Poset )
5 lublecl.x 
 |-  ( ph -> X e. B )
6 breq1 
 |-  ( y = z -> ( y .<_ X <-> z .<_ X ) )
7 6 ralrab 
 |-  ( A. z e. { y e. B | y .<_ X } z .<_ x <-> A. z e. B ( z .<_ X -> z .<_ x ) )
8 6 ralrab 
 |-  ( A. z e. { y e. B | y .<_ X } z .<_ w <-> A. z e. B ( z .<_ X -> z .<_ w ) )
9 8 imbi1i 
 |-  ( ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) <-> ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) )
10 9 ralbii 
 |-  ( A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) <-> A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) )
11 7 10 anbi12i 
 |-  ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> ( A. z e. B ( z .<_ X -> z .<_ x ) /\ A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) ) )
12 1 2 posref 
 |-  ( ( K e. Poset /\ X e. B ) -> X .<_ X )
13 4 5 12 syl2anc 
 |-  ( ph -> X .<_ X )
14 breq1 
 |-  ( z = X -> ( z .<_ X <-> X .<_ X ) )
15 breq1 
 |-  ( z = X -> ( z .<_ x <-> X .<_ x ) )
16 14 15 imbi12d 
 |-  ( z = X -> ( ( z .<_ X -> z .<_ x ) <-> ( X .<_ X -> X .<_ x ) ) )
17 16 rspcva 
 |-  ( ( X e. B /\ A. z e. B ( z .<_ X -> z .<_ x ) ) -> ( X .<_ X -> X .<_ x ) )
18 13 17 syl5com 
 |-  ( ph -> ( ( X e. B /\ A. z e. B ( z .<_ X -> z .<_ x ) ) -> X .<_ x ) )
19 5 18 mpand 
 |-  ( ph -> ( A. z e. B ( z .<_ X -> z .<_ x ) -> X .<_ x ) )
20 19 adantr 
 |-  ( ( ph /\ x e. B ) -> ( A. z e. B ( z .<_ X -> z .<_ x ) -> X .<_ x ) )
21 idd 
 |-  ( z e. B -> ( z .<_ X -> z .<_ X ) )
22 21 rgen 
 |-  A. z e. B ( z .<_ X -> z .<_ X )
23 breq2 
 |-  ( w = X -> ( z .<_ w <-> z .<_ X ) )
24 23 imbi2d 
 |-  ( w = X -> ( ( z .<_ X -> z .<_ w ) <-> ( z .<_ X -> z .<_ X ) ) )
25 24 ralbidv 
 |-  ( w = X -> ( A. z e. B ( z .<_ X -> z .<_ w ) <-> A. z e. B ( z .<_ X -> z .<_ X ) ) )
26 breq2 
 |-  ( w = X -> ( x .<_ w <-> x .<_ X ) )
27 25 26 imbi12d 
 |-  ( w = X -> ( ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) <-> ( A. z e. B ( z .<_ X -> z .<_ X ) -> x .<_ X ) ) )
28 27 rspcv 
 |-  ( X e. B -> ( A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) -> ( A. z e. B ( z .<_ X -> z .<_ X ) -> x .<_ X ) ) )
29 5 28 syl 
 |-  ( ph -> ( A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) -> ( A. z e. B ( z .<_ X -> z .<_ X ) -> x .<_ X ) ) )
30 22 29 mpii 
 |-  ( ph -> ( A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) -> x .<_ X ) )
31 30 adantr 
 |-  ( ( ph /\ x e. B ) -> ( A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) -> x .<_ X ) )
32 4 adantr 
 |-  ( ( ph /\ x e. B ) -> K e. Poset )
33 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
34 5 adantr 
 |-  ( ( ph /\ x e. B ) -> X e. B )
35 1 2 posasymb 
 |-  ( ( K e. Poset /\ x e. B /\ X e. B ) -> ( ( x .<_ X /\ X .<_ x ) <-> x = X ) )
36 32 33 34 35 syl3anc 
 |-  ( ( ph /\ x e. B ) -> ( ( x .<_ X /\ X .<_ x ) <-> x = X ) )
37 36 biimpd 
 |-  ( ( ph /\ x e. B ) -> ( ( x .<_ X /\ X .<_ x ) -> x = X ) )
38 37 ancomsd 
 |-  ( ( ph /\ x e. B ) -> ( ( X .<_ x /\ x .<_ X ) -> x = X ) )
39 20 31 38 syl2and 
 |-  ( ( ph /\ x e. B ) -> ( ( A. z e. B ( z .<_ X -> z .<_ x ) /\ A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) ) -> x = X ) )
40 breq2 
 |-  ( x = X -> ( z .<_ x <-> z .<_ X ) )
41 40 biimprd 
 |-  ( x = X -> ( z .<_ X -> z .<_ x ) )
42 41 ralrimivw 
 |-  ( x = X -> A. z e. B ( z .<_ X -> z .<_ x ) )
43 42 adantl 
 |-  ( ( ( ph /\ x e. B ) /\ x = X ) -> A. z e. B ( z .<_ X -> z .<_ x ) )
44 5 adantr 
 |-  ( ( ph /\ x = X ) -> X e. B )
45 breq1 
 |-  ( z = X -> ( z .<_ w <-> X .<_ w ) )
46 14 45 imbi12d 
 |-  ( z = X -> ( ( z .<_ X -> z .<_ w ) <-> ( X .<_ X -> X .<_ w ) ) )
47 46 rspcva 
 |-  ( ( X e. B /\ A. z e. B ( z .<_ X -> z .<_ w ) ) -> ( X .<_ X -> X .<_ w ) )
48 pm5.5 
 |-  ( X .<_ X -> ( ( X .<_ X -> X .<_ w ) <-> X .<_ w ) )
49 13 48 syl 
 |-  ( ph -> ( ( X .<_ X -> X .<_ w ) <-> X .<_ w ) )
50 breq1 
 |-  ( x = X -> ( x .<_ w <-> X .<_ w ) )
51 50 bicomd 
 |-  ( x = X -> ( X .<_ w <-> x .<_ w ) )
52 49 51 sylan9bb 
 |-  ( ( ph /\ x = X ) -> ( ( X .<_ X -> X .<_ w ) <-> x .<_ w ) )
53 47 52 imbitrid 
 |-  ( ( ph /\ x = X ) -> ( ( X e. B /\ A. z e. B ( z .<_ X -> z .<_ w ) ) -> x .<_ w ) )
54 44 53 mpand 
 |-  ( ( ph /\ x = X ) -> ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) )
55 54 ralrimivw 
 |-  ( ( ph /\ x = X ) -> A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) )
56 55 adantlr 
 |-  ( ( ( ph /\ x e. B ) /\ x = X ) -> A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) )
57 43 56 jca 
 |-  ( ( ( ph /\ x e. B ) /\ x = X ) -> ( A. z e. B ( z .<_ X -> z .<_ x ) /\ A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) ) )
58 57 ex 
 |-  ( ( ph /\ x e. B ) -> ( x = X -> ( A. z e. B ( z .<_ X -> z .<_ x ) /\ A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) ) ) )
59 39 58 impbid 
 |-  ( ( ph /\ x e. B ) -> ( ( A. z e. B ( z .<_ X -> z .<_ x ) /\ A. w e. B ( A. z e. B ( z .<_ X -> z .<_ w ) -> x .<_ w ) ) <-> x = X ) )
60 11 59 bitrid 
 |-  ( ( ph /\ x e. B ) -> ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )