Metamath Proof Explorer

Theorem tosglblem

Description: Lemma for tosglb and xrsclat . (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by NM, 15-Sep-2018)

Ref Expression
Hypotheses tosglb.b ⊢B=BaseK
tosglb.l ⊢<˙=<K
tosglb.1 ⊢φ→K∈Toset
tosglb.2 ⊢φ→A⊆B
tosglb.e ⊢≤˙=≤K
Assertion tosglblem ⊢φ∧a∈B→∀b∈Aa≤˙b∧∀c∈B∀b∈Ac≤˙b→c≤˙a↔∀b∈A¬a<˙-1b∧∀b∈Bb<˙-1a→∃d∈Ab<˙-1d

Proof

Step Hyp Ref Expression
1 tosglb.b ⊢B=BaseK
2 tosglb.l ⊢<˙=<K
3 tosglb.1 ⊢φ→K∈Toset
4 tosglb.2 ⊢φ→A⊆B
5 tosglb.e ⊢≤˙=≤K
6 3 ad2antrr ⊢φ∧a∈B∧b∈A→K∈Toset
7 4 adantr ⊢φ∧a∈B→A⊆B
8 7 sselda ⊢φ∧a∈B∧b∈A→b∈B
9 simplr ⊢φ∧a∈B∧b∈A→a∈B
10 1 5 2 tltnle ⊢K∈Toset∧b∈B∧a∈B→b<˙a↔¬a≤˙b
11 6 8 9 10 syl3anc ⊢φ∧a∈B∧b∈A→b<˙a↔¬a≤˙b
12 11 con2bid ⊢φ∧a∈B∧b∈A→a≤˙b↔¬b<˙a
13 12 ralbidva ⊢φ∧a∈B→∀b∈Aa≤˙b↔∀b∈A¬b<˙a
14 4 ad2antrr ⊢φ∧c∈B∧b∈A→A⊆B
15 simpr ⊢φ∧c∈B∧b∈A→b∈A
16 14 15 sseldd ⊢φ∧c∈B∧b∈A→b∈B
17 1 5 2 tltnle ⊢K∈Toset∧b∈B∧c∈B→b<˙c↔¬c≤˙b
18 3 17 syl3an1 ⊢φ∧b∈B∧c∈B→b<˙c↔¬c≤˙b
19 18 3com23 ⊢φ∧c∈B∧b∈B→b<˙c↔¬c≤˙b
20 19 3expa ⊢φ∧c∈B∧b∈B→b<˙c↔¬c≤˙b
21 20 con2bid ⊢φ∧c∈B∧b∈B→c≤˙b↔¬b<˙c
22 16 21 syldan ⊢φ∧c∈B∧b∈A→c≤˙b↔¬b<˙c
23 22 ralbidva ⊢φ∧c∈B→∀b∈Ac≤˙b↔∀b∈A¬b<˙c
24 breq1 ⊢b=d→b<˙c↔d<˙c
25 24 notbid ⊢b=d→¬b<˙c↔¬d<˙c
26 25 cbvralvw ⊢∀b∈A¬b<˙c↔∀d∈A¬d<˙c
27 ralnex ⊢∀d∈A¬d<˙c↔¬∃d∈Ad<˙c
28 26 27 bitri ⊢∀b∈A¬b<˙c↔¬∃d∈Ad<˙c
29 23 28 bitrdi ⊢φ∧c∈B→∀b∈Ac≤˙b↔¬∃d∈Ad<˙c
30 29 adantlr ⊢φ∧a∈B∧c∈B→∀b∈Ac≤˙b↔¬∃d∈Ad<˙c
31 3 ad2antrr ⊢φ∧a∈B∧c∈B→K∈Toset
32 simplr ⊢φ∧a∈B∧c∈B→a∈B
33 simpr ⊢φ∧a∈B∧c∈B→c∈B
34 1 5 2 tltnle ⊢K∈Toset∧a∈B∧c∈B→a<˙c↔¬c≤˙a
35 31 32 33 34 syl3anc ⊢φ∧a∈B∧c∈B→a<˙c↔¬c≤˙a
36 35 con2bid ⊢φ∧a∈B∧c∈B→c≤˙a↔¬a<˙c
37 30 36 imbi12d ⊢φ∧a∈B∧c∈B→∀b∈Ac≤˙b→c≤˙a↔¬∃d∈Ad<˙c→¬a<˙c
38 con34b ⊢a<˙c→∃d∈Ad<˙c↔¬∃d∈Ad<˙c→¬a<˙c
39 37 38 bitr4di ⊢φ∧a∈B∧c∈B→∀b∈Ac≤˙b→c≤˙a↔a<˙c→∃d∈Ad<˙c
40 39 ralbidva ⊢φ∧a∈B→∀c∈B∀b∈Ac≤˙b→c≤˙a↔∀c∈Ba<˙c→∃d∈Ad<˙c
41 breq2 ⊢b=c→a<˙b↔a<˙c
42 breq2 ⊢b=c→d<˙b↔d<˙c
43 42 rexbidv ⊢b=c→∃d∈Ad<˙b↔∃d∈Ad<˙c
44 41 43 imbi12d ⊢b=c→a<˙b→∃d∈Ad<˙b↔a<˙c→∃d∈Ad<˙c
45 44 cbvralvw ⊢∀b∈Ba<˙b→∃d∈Ad<˙b↔∀c∈Ba<˙c→∃d∈Ad<˙c
46 40 45 bitr4di ⊢φ∧a∈B→∀c∈B∀b∈Ac≤˙b→c≤˙a↔∀b∈Ba<˙b→∃d∈Ad<˙b
47 13 46 anbi12d ⊢φ∧a∈B→∀b∈Aa≤˙b∧∀c∈B∀b∈Ac≤˙b→c≤˙a↔∀b∈A¬b<˙a∧∀b∈Ba<˙b→∃d∈Ad<˙b
48 vex ⊢a∈V
49 vex ⊢b∈V
50 48 49 brcnv ⊢a<˙-1b↔b<˙a
51 50 notbii ⊢¬a<˙-1b↔¬b<˙a
52 51 ralbii ⊢∀b∈A¬a<˙-1b↔∀b∈A¬b<˙a
53 49 48 brcnv ⊢b<˙-1a↔a<˙b
54 vex ⊢d∈V
55 49 54 brcnv ⊢b<˙-1d↔d<˙b
56 55 rexbii ⊢∃d∈Ab<˙-1d↔∃d∈Ad<˙b
57 53 56 imbi12i ⊢b<˙-1a→∃d∈Ab<˙-1d↔a<˙b→∃d∈Ad<˙b
58 57 ralbii ⊢∀b∈Bb<˙-1a→∃d∈Ab<˙-1d↔∀b∈Ba<˙b→∃d∈Ad<˙b
59 52 58 anbi12i ⊢∀b∈A¬a<˙-1b∧∀b∈Bb<˙-1a→∃d∈Ab<˙-1d↔∀b∈A¬b<˙a∧∀b∈Ba<˙b→∃d∈Ad<˙b
60 47 59 bitr4di ⊢φ∧a∈B→∀b∈Aa≤˙b∧∀c∈B∀b∈Ac≤˙b→c≤˙a↔∀b∈A¬a<˙-1b∧∀b∈Bb<˙-1a→∃d∈Ab<˙-1d