Metamath Proof Explorer


Theorem isbasisrelowllem2

Description: Lemma for isbasisrelowl . (Contributed by ML, 27-Jul-2020)

Ref Expression
Hypothesis isbasisrelowl.1 I = . 2
Assertion isbasisrelowllem2 a b x = z | a z z < b c d y = z | c z z < d a c d b x y I

Proof

Step Hyp Ref Expression
1 isbasisrelowl.1 I = . 2
2 simplr1 a b x = z | a z z < b c d y = z | c z z < d a c d b c
3 simplr2 a b x = z | a z z < b c d y = z | c z z < d a c d b d
4 nfv z a
5 nfv z b
6 nfrab1 _ z z | a z z < b
7 6 nfeq2 z x = z | a z z < b
8 4 5 7 nf3an z a b x = z | a z z < b
9 nfv z c
10 nfv z d
11 nfrab1 _ z z | c z z < d
12 11 nfeq2 z y = z | c z z < d
13 9 10 12 nf3an z c d y = z | c z z < d
14 8 13 nfan z a b x = z | a z z < b c d y = z | c z z < d
15 nfv z a c d b
16 14 15 nfan z a b x = z | a z z < b c d y = z | c z z < d a c d b
17 nfcv _ z x y
18 simp3 a b x = z | a z z < b x = z | a z z < b
19 simp3 c d y = z | c z z < d y = z | c z z < d
20 elin z x y z x z y
21 eleq2 x = z | a z z < b z x z z | a z z < b
22 rabid z z | a z z < b z a z z < b
23 21 22 bitrdi x = z | a z z < b z x z a z z < b
24 23 anbi1d x = z | a z z < b z x z y z a z z < b z y
25 20 24 syl5bb x = z | a z z < b z x y z a z z < b z y
26 eleq2 y = z | c z z < d z y z z | c z z < d
27 rabid z z | c z z < d z c z z < d
28 26 27 bitrdi y = z | c z z < d z y z c z z < d
29 28 anbi2d y = z | c z z < d z a z z < b z y z a z z < b z c z z < d
30 25 29 sylan9bb x = z | a z z < b y = z | c z z < d z x y z a z z < b z c z z < d
31 an4 z a z z < b z c z z < d z z a z z < b c z z < d
32 anidm z z z
33 32 anbi1i z z a z z < b c z z < d z a z z < b c z z < d
34 31 33 bitri z a z z < b z c z z < d z a z z < b c z z < d
35 an4 a z z < d c z z < b a z c z z < d z < b
36 an42 a z z < b c z z < d a z c z z < d z < b
37 36 bicomi a z c z z < d z < b a z z < b c z z < d
38 35 37 bitri a z z < d c z z < b a z z < b c z z < d
39 38 bicomi a z z < b c z z < d a z z < d c z z < b
40 39 anbi2i z a z z < b c z z < d z a z z < d c z z < b
41 34 40 bitri z a z z < b z c z z < d z a z z < d c z z < b
42 30 41 bitrdi x = z | a z z < b y = z | c z z < d z x y z a z z < d c z z < b
43 18 19 42 syl2an a b x = z | a z z < b c d y = z | c z z < d z x y z a z z < d c z z < b
44 43 adantr a b x = z | a z z < b c d y = z | c z z < d a c d b z x y z a z z < d c z z < b
45 simpl z a z z < d c z z < b z
46 simprrl z a z z < d c z z < b c z
47 simprlr z a z z < d c z z < b z < d
48 45 46 47 jca32 z a z z < d c z z < b z c z z < d
49 44 48 syl6bi a b x = z | a z z < b c d y = z | c z z < d a c d b z x y z c z z < d
50 3simpa a b x = z | a z z < b a b
51 3simpa c d y = z | c z z < d c d
52 50 51 anim12i a b x = z | a z z < b c d y = z | c z z < d a b c d
53 letr a c z a c c z a z
54 53 3expia a c z a c c z a z
55 54 exp4a a c z a c c z a z
56 55 ad2ant2r a b c d z a c c z a z
57 ltletr z d b z < d d b z < b
58 57 3com13 b d z z < d d b z < b
59 58 expcomd b d z d b z < d z < b
60 59 3expia b d z d b z < d z < b
61 60 ad2ant2l a b c d z d b z < d z < b
62 56 61 jcad a b c d z a c c z a z d b z < d z < b
63 anim12 a c c z a z d b z < d z < b a c d b c z a z z < d z < b
64 62 63 syl6 a b c d z a c d b c z a z z < d z < b
65 64 com23 a b c d a c d b z c z a z z < d z < b
66 anim12 c z a z z < d z < b c z z < d a z z < b
67 65 66 syl8 a b c d a c d b z c z z < d a z z < b
68 67 imp31 a b c d a c d b z c z z < d a z z < b
69 68 ancrd a b c d a c d b z c z z < d a z z < b c z z < d
70 an42 a z z < d c z z < b a z c z z < b z < d
71 an4 a z c z z < b z < d a z z < b c z z < d
72 70 71 bitri a z z < d c z z < b a z z < b c z z < d
73 69 72 syl6ibr a b c d a c d b z c z z < d a z z < d c z z < b
74 simpr a b c d a c d b z z
75 73 74 jctild a b c d a c d b z c z z < d z a z z < d c z z < b
76 52 75 sylanl1 a b x = z | a z z < b c d y = z | c z z < d a c d b z c z z < d z a z z < d c z z < b
77 76 imp a b x = z | a z z < b c d y = z | c z z < d a c d b z c z z < d z a z z < d c z z < b
78 77 an32s a b x = z | a z z < b c d y = z | c z z < d a c d b c z z < d z z a z z < d c z z < b
79 44 adantr a b x = z | a z z < b c d y = z | c z z < d a c d b c z z < d z x y z a z z < d c z z < b
80 79 adantr a b x = z | a z z < b c d y = z | c z z < d a c d b c z z < d z z x y z a z z < d c z z < b
81 78 80 mpbird a b x = z | a z z < b c d y = z | c z z < d a c d b c z z < d z z x y
82 81 expl a b x = z | a z z < b c d y = z | c z z < d a c d b c z z < d z z x y
83 82 ancomsd a b x = z | a z z < b c d y = z | c z z < d a c d b z c z z < d z x y
84 49 83 impbid a b x = z | a z z < b c d y = z | c z z < d a c d b z x y z c z z < d
85 84 27 bitr4di a b x = z | a z z < b c d y = z | c z z < d a c d b z x y z z | c z z < d
86 16 17 11 85 eqrd a b x = z | a z z < b c d y = z | c z z < d a c d b x y = z | c z z < d
87 3 86 jca a b x = z | a z z < b c d y = z | c z z < d a c d b d x y = z | c z z < d
88 87 19.8ad a b x = z | a z z < b c d y = z | c z z < d a c d b d d x y = z | c z z < d
89 df-rex d x y = z | c z z < d d d x y = z | c z z < d
90 88 89 sylibr a b x = z | a z z < b c d y = z | c z z < d a c d b d x y = z | c z z < d
91 2 90 jca a b x = z | a z z < b c d y = z | c z z < d a c d b c d x y = z | c z z < d
92 91 19.8ad a b x = z | a z z < b c d y = z | c z z < d a c d b c c d x y = z | c z z < d
93 df-rex c d x y = z | c z z < d c c d x y = z | c z z < d
94 92 93 sylibr a b x = z | a z z < b c d y = z | c z z < d a c d b c d x y = z | c z z < d
95 1 icoreelrnab x y I c d x y = z | c z z < d
96 94 95 sylibr a b x = z | a z z < b c d y = z | c z z < d a c d b x y I