Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexprlem1ssl GIF version

Theorem recexprlem1ssl 6605
 Description: The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
Assertion
Ref Expression
recexprlem1ssl (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlem1ssl
Dummy variables z w v u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1prl 6536 . . . 4 (1st ‘1P) = {ww <Q 1Q}
21abeq2i 2145 . . 3 (w (1st ‘1P) ↔ w <Q 1Q)
3 rec1nq 6379 . . . . . . 7 (*Q‘1Q) = 1Q
4 ltrnqi 6404 . . . . . . 7 (w <Q 1Q → (*Q‘1Q) <Q (*Qw))
53, 4syl5eqbrr 3789 . . . . . 6 (w <Q 1Q → 1Q <Q (*Qw))
6 prop 6458 . . . . . . 7 (A P → ⟨(1stA), (2ndA)⟩ P)
7 prmuloc2 6548 . . . . . . 7 ((⟨(1stA), (2ndA)⟩ P 1Q <Q (*Qw)) → v (1stA)(v ·Q (*Qw)) (2ndA))
86, 7sylan 267 . . . . . 6 ((A P 1Q <Q (*Qw)) → v (1stA)(v ·Q (*Qw)) (2ndA))
95, 8sylan2 270 . . . . 5 ((A P w <Q 1Q) → v (1stA)(v ·Q (*Qw)) (2ndA))
10 prnmaxl 6471 . . . . . . . 8 ((⟨(1stA), (2ndA)⟩ P v (1stA)) → z (1stA)v <Q z)
116, 10sylan 267 . . . . . . 7 ((A P v (1stA)) → z (1stA)v <Q z)
1211ad2ant2r 478 . . . . . 6 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → z (1stA)v <Q z)
13 elprnql 6464 . . . . . . . . . . . . . 14 ((⟨(1stA), (2ndA)⟩ P v (1stA)) → v Q)
146, 13sylan 267 . . . . . . . . . . . . 13 ((A P v (1stA)) → v Q)
1514ad2ant2r 478 . . . . . . . . . . . 12 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → v Q)
16153adant3 923 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → v Q)
17 simp1r 928 . . . . . . . . . . . 12 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → w <Q 1Q)
18 ltrelnq 6349 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
1918brel 4335 . . . . . . . . . . . . 13 (w <Q 1Q → (w Q 1Q Q))
2019simpld 105 . . . . . . . . . . . 12 (w <Q 1Qw Q)
2117, 20syl 14 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → w Q)
22 simp3 905 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → v <Q z)
23 simp2r 930 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → (v ·Q (*Qw)) (2ndA))
24 simpr 103 . . . . . . . . . . . 12 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (v <Q z (v ·Q (*Qw)) (2ndA)))
25 ltrnqi 6404 . . . . . . . . . . . . . 14 (v <Q z → (*Qz) <Q (*Qv))
26 ltmnqg 6385 . . . . . . . . . . . . . . . 16 ((f Q g Q Q) → (f <Q g ↔ ( ·Q f) <Q ( ·Q g)))
2726adantl 262 . . . . . . . . . . . . . . 15 ((((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) (f Q g Q Q)) → (f <Q g ↔ ( ·Q f) <Q ( ·Q g)))
28 simprl 483 . . . . . . . . . . . . . . . 16 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → v <Q z)
2918brel 4335 . . . . . . . . . . . . . . . . 17 (v <Q z → (v Q z Q))
3029simprd 107 . . . . . . . . . . . . . . . 16 (v <Q zz Q)
31 recclnq 6376 . . . . . . . . . . . . . . . 16 (z Q → (*Qz) Q)
3228, 30, 313syl 17 . . . . . . . . . . . . . . 15 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (*Qz) Q)
33 recclnq 6376 . . . . . . . . . . . . . . . 16 (v Q → (*Qv) Q)
3433ad2antrr 457 . . . . . . . . . . . . . . 15 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (*Qv) Q)
35 simplr 482 . . . . . . . . . . . . . . 15 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → w Q)
36 mulcomnqg 6367 . . . . . . . . . . . . . . . 16 ((f Q g Q) → (f ·Q g) = (g ·Q f))
3736adantl 262 . . . . . . . . . . . . . . 15 ((((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) (f Q g Q)) → (f ·Q g) = (g ·Q f))
3827, 32, 34, 35, 37caovord2d 5612 . . . . . . . . . . . . . 14 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((*Qz) <Q (*Qv) ↔ ((*Qz) ·Q w) <Q ((*Qv) ·Q w)))
3925, 38syl5ib 143 . . . . . . . . . . . . 13 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (v <Q z → ((*Qz) ·Q w) <Q ((*Qv) ·Q w)))
40 1nq 6350 . . . . . . . . . . . . . . . . . 18 1Q Q
41 mulidnq 6373 . . . . . . . . . . . . . . . . . 18 (1Q Q → (1Q ·Q 1Q) = 1Q)
4240, 41ax-mp 7 . . . . . . . . . . . . . . . . 17 (1Q ·Q 1Q) = 1Q
43 mulcomnqg 6367 . . . . . . . . . . . . . . . . . . . . . 22 ((v Q (*Qv) Q) → (v ·Q (*Qv)) = ((*Qv) ·Q v))
4433, 43mpdan 398 . . . . . . . . . . . . . . . . . . . . 21 (v Q → (v ·Q (*Qv)) = ((*Qv) ·Q v))
45 recidnq 6377 . . . . . . . . . . . . . . . . . . . . 21 (v Q → (v ·Q (*Qv)) = 1Q)
4644, 45eqtr3d 2071 . . . . . . . . . . . . . . . . . . . 20 (v Q → ((*Qv) ·Q v) = 1Q)
47 recidnq 6377 . . . . . . . . . . . . . . . . . . . 20 (w Q → (w ·Q (*Qw)) = 1Q)
4846, 47oveqan12d 5474 . . . . . . . . . . . . . . . . . . 19 ((v Q w Q) → (((*Qv) ·Q v) ·Q (w ·Q (*Qw))) = (1Q ·Q 1Q))
4948adantr 261 . . . . . . . . . . . . . . . . . 18 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (((*Qv) ·Q v) ·Q (w ·Q (*Qw))) = (1Q ·Q 1Q))
50 simpll 481 . . . . . . . . . . . . . . . . . . 19 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → v Q)
51 mulassnqg 6368 . . . . . . . . . . . . . . . . . . . 20 ((f Q g Q Q) → ((f ·Q g) ·Q ) = (f ·Q (g ·Q )))
5251adantl 262 . . . . . . . . . . . . . . . . . . 19 ((((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) (f Q g Q Q)) → ((f ·Q g) ·Q ) = (f ·Q (g ·Q )))
53 recclnq 6376 . . . . . . . . . . . . . . . . . . . 20 (w Q → (*Qw) Q)
5435, 53syl 14 . . . . . . . . . . . . . . . . . . 19 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (*Qw) Q)
55 mulclnq 6360 . . . . . . . . . . . . . . . . . . . 20 ((f Q g Q) → (f ·Q g) Q)
5655adantl 262 . . . . . . . . . . . . . . . . . . 19 ((((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) (f Q g Q)) → (f ·Q g) Q)
5734, 50, 35, 37, 52, 54, 56caov4d 5627 . . . . . . . . . . . . . . . . . 18 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (((*Qv) ·Q v) ·Q (w ·Q (*Qw))) = (((*Qv) ·Q w) ·Q (v ·Q (*Qw))))
5849, 57eqtr3d 2071 . . . . . . . . . . . . . . . . 17 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (1Q ·Q 1Q) = (((*Qv) ·Q w) ·Q (v ·Q (*Qw))))
5942, 58syl5reqr 2084 . . . . . . . . . . . . . . . 16 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (((*Qv) ·Q w) ·Q (v ·Q (*Qw))) = 1Q)
60 mulclnq 6360 . . . . . . . . . . . . . . . . . . 19 (((*Qv) Q w Q) → ((*Qv) ·Q w) Q)
6133, 60sylan 267 . . . . . . . . . . . . . . . . . 18 ((v Q w Q) → ((*Qv) ·Q w) Q)
62 mulclnq 6360 . . . . . . . . . . . . . . . . . . 19 ((v Q (*Qw) Q) → (v ·Q (*Qw)) Q)
6353, 62sylan2 270 . . . . . . . . . . . . . . . . . 18 ((v Q w Q) → (v ·Q (*Qw)) Q)
64 recmulnqg 6375 . . . . . . . . . . . . . . . . . 18 ((((*Qv) ·Q w) Q (v ·Q (*Qw)) Q) → ((*Q‘((*Qv) ·Q w)) = (v ·Q (*Qw)) ↔ (((*Qv) ·Q w) ·Q (v ·Q (*Qw))) = 1Q))
6561, 63, 64syl2anc 391 . . . . . . . . . . . . . . . . 17 ((v Q w Q) → ((*Q‘((*Qv) ·Q w)) = (v ·Q (*Qw)) ↔ (((*Qv) ·Q w) ·Q (v ·Q (*Qw))) = 1Q))
6665adantr 261 . . . . . . . . . . . . . . . 16 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((*Q‘((*Qv) ·Q w)) = (v ·Q (*Qw)) ↔ (((*Qv) ·Q w) ·Q (v ·Q (*Qw))) = 1Q))
6759, 66mpbird 156 . . . . . . . . . . . . . . 15 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (*Q‘((*Qv) ·Q w)) = (v ·Q (*Qw)))
6867eleq1d 2103 . . . . . . . . . . . . . 14 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((*Q‘((*Qv) ·Q w)) (2ndA) ↔ (v ·Q (*Qw)) (2ndA)))
6968biimprd 147 . . . . . . . . . . . . 13 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((v ·Q (*Qw)) (2ndA) → (*Q‘((*Qv) ·Q w)) (2ndA)))
70 breq2 3759 . . . . . . . . . . . . . . . . . 18 (y = ((*Qv) ·Q w) → (((*Qz) ·Q w) <Q y ↔ ((*Qz) ·Q w) <Q ((*Qv) ·Q w)))
71 fveq2 5121 . . . . . . . . . . . . . . . . . . 19 (y = ((*Qv) ·Q w) → (*Qy) = (*Q‘((*Qv) ·Q w)))
7271eleq1d 2103 . . . . . . . . . . . . . . . . . 18 (y = ((*Qv) ·Q w) → ((*Qy) (2ndA) ↔ (*Q‘((*Qv) ·Q w)) (2ndA)))
7370, 72anbi12d 442 . . . . . . . . . . . . . . . . 17 (y = ((*Qv) ·Q w) → ((((*Qz) ·Q w) <Q y (*Qy) (2ndA)) ↔ (((*Qz) ·Q w) <Q ((*Qv) ·Q w) (*Q‘((*Qv) ·Q w)) (2ndA))))
7473spcegv 2635 . . . . . . . . . . . . . . . 16 (((*Qv) ·Q w) Q → ((((*Qz) ·Q w) <Q ((*Qv) ·Q w) (*Q‘((*Qv) ·Q w)) (2ndA)) → y(((*Qz) ·Q w) <Q y (*Qy) (2ndA))))
7561, 74syl 14 . . . . . . . . . . . . . . 15 ((v Q w Q) → ((((*Qz) ·Q w) <Q ((*Qv) ·Q w) (*Q‘((*Qv) ·Q w)) (2ndA)) → y(((*Qz) ·Q w) <Q y (*Qy) (2ndA))))
76 recexpr.1 . . . . . . . . . . . . . . . 16 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
7776recexprlemell 6594 . . . . . . . . . . . . . . 15 (((*Qz) ·Q w) (1stB) ↔ y(((*Qz) ·Q w) <Q y (*Qy) (2ndA)))
7875, 77syl6ibr 151 . . . . . . . . . . . . . 14 ((v Q w Q) → ((((*Qz) ·Q w) <Q ((*Qv) ·Q w) (*Q‘((*Qv) ·Q w)) (2ndA)) → ((*Qz) ·Q w) (1stB)))
7978adantr 261 . . . . . . . . . . . . 13 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((((*Qz) ·Q w) <Q ((*Qv) ·Q w) (*Q‘((*Qv) ·Q w)) (2ndA)) → ((*Qz) ·Q w) (1stB)))
8039, 69, 79syl2and 279 . . . . . . . . . . . 12 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((v <Q z (v ·Q (*Qw)) (2ndA)) → ((*Qz) ·Q w) (1stB)))
8124, 80mpd 13 . . . . . . . . . . 11 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → ((*Qz) ·Q w) (1stB))
8216, 21, 22, 23, 81syl22anc 1135 . . . . . . . . . 10 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → ((*Qz) ·Q w) (1stB))
83303ad2ant3 926 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → z Q)
84 mulidnq 6373 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = w)
85 mulcomnqg 6367 . . . . . . . . . . . . . . 15 ((w Q 1Q Q) → (w ·Q 1Q) = (1Q ·Q w))
8640, 85mpan2 401 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = (1Q ·Q w))
8784, 86eqtr3d 2071 . . . . . . . . . . . . 13 (w Qw = (1Q ·Q w))
8887adantl 262 . . . . . . . . . . . 12 ((z Q w Q) → w = (1Q ·Q w))
89 recidnq 6377 . . . . . . . . . . . . . 14 (z Q → (z ·Q (*Qz)) = 1Q)
9089oveq1d 5470 . . . . . . . . . . . . 13 (z Q → ((z ·Q (*Qz)) ·Q w) = (1Q ·Q w))
9190adantr 261 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (1Q ·Q w))
92 mulassnqg 6368 . . . . . . . . . . . . . 14 ((z Q (*Qz) Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9331, 92syl3an2 1168 . . . . . . . . . . . . 13 ((z Q z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
94933anidm12 1191 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9588, 91, 943eqtr2d 2075 . . . . . . . . . . 11 ((z Q w Q) → w = (z ·Q ((*Qz) ·Q w)))
9683, 21, 95syl2anc 391 . . . . . . . . . 10 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → w = (z ·Q ((*Qz) ·Q w)))
97 oveq2 5463 . . . . . . . . . . . 12 (x = ((*Qz) ·Q w) → (z ·Q x) = (z ·Q ((*Qz) ·Q w)))
9897eqeq2d 2048 . . . . . . . . . . 11 (x = ((*Qz) ·Q w) → (w = (z ·Q x) ↔ w = (z ·Q ((*Qz) ·Q w))))
9998rspcev 2650 . . . . . . . . . 10 ((((*Qz) ·Q w) (1stB) w = (z ·Q ((*Qz) ·Q w))) → x (1stB)w = (z ·Q x))
10082, 96, 99syl2anc 391 . . . . . . . . 9 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → x (1stB)w = (z ·Q x))
1011003expia 1105 . . . . . . . 8 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → (v <Q zx (1stB)w = (z ·Q x)))
102101reximdv 2414 . . . . . . 7 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → (z (1stA)v <Q zz (1stA)x (1stB)w = (z ·Q x)))
10376recexprlempr 6604 . . . . . . . . 9 (A PB P)
104 df-imp 6452 . . . . . . . . . 10 ·P = (y P, w P ↦ ⟨{u Qf Q g Q (f (1sty) g (1stw) u = (f ·Q g))}, {u Qf Q g Q (f (2ndy) g (2ndw) u = (f ·Q g))}⟩)
105104, 55genpelvl 6495 . . . . . . . . 9 ((A P B P) → (w (1st ‘(A ·P B)) ↔ z (1stA)x (1stB)w = (z ·Q x)))
106103, 105mpdan 398 . . . . . . . 8 (A P → (w (1st ‘(A ·P B)) ↔ z (1stA)x (1stB)w = (z ·Q x)))
107106ad2antrr 457 . . . . . . 7 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → (w (1st ‘(A ·P B)) ↔ z (1stA)x (1stB)w = (z ·Q x)))
108102, 107sylibrd 158 . . . . . 6 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → (z (1stA)v <Q zw (1st ‘(A ·P B))))
10912, 108mpd 13 . . . . 5 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → w (1st ‘(A ·P B)))
1109, 109rexlimddv 2431 . . . 4 ((A P w <Q 1Q) → w (1st ‘(A ·P B)))
111110ex 108 . . 3 (A P → (w <Q 1Qw (1st ‘(A ·P B))))
1122, 111syl5bi 141 . 2 (A P → (w (1st ‘1P) → w (1st ‘(A ·P B))))
113112ssrdv 2945 1 (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  1Qc1q 6265   ·Q cmq 6267  *Qcrq 6268
 Copyright terms: Public domain W3C validator