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

Theorem recexprlem1ssl 6454
Description: The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6459. (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 6391 . . . 4 (1st ‘1P) = {ww <Q 1Q}
21abeq2i 2121 . . 3 (w (1st ‘1P) ↔ w <Q 1Q)
3 rec1nq 6240 . . . . . . 7 (*Q‘1Q) = 1Q
4 ltrnqi 6264 . . . . . . 7 (w <Q 1Q → (*Q‘1Q) <Q (*Qw))
53, 4syl5eqbrr 3761 . . . . . 6 (w <Q 1Q → 1Q <Q (*Qw))
6 prop 6315 . . . . . . 7 (A P → ⟨(1stA), (2ndA)⟩ P)
7 prmuloc2 6397 . . . . . . 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 6328 . . . . . . . 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 463 . . . . . 6 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → z (1stA)v <Q z)
13 elprnql 6321 . . . . . . . . . . . . . 14 ((⟨(1stA), (2ndA)⟩ P v (1stA)) → v Q)
146, 13sylan 267 . . . . . . . . . . . . 13 ((A P v (1stA)) → v Q)
1514ad2ant2r 463 . . . . . . . . . . . 12 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → v Q)
16153adant3 906 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → v Q)
17 simp1r 911 . . . . . . . . . . . 12 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → w <Q 1Q)
18 ltrelnq 6210 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
1918brel 4307 . . . . . . . . . . . . 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 888 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → v <Q z)
23 simp2r 913 . . . . . . . . . . 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 6264 . . . . . . . . . . . . . 14 (v <Q z → (*Qz) <Q (*Qv))
26 ltmnqg 6246 . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . 16 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → v <Q z)
2918brel 4307 . . . . . . . . . . . . . . . . 17 (v <Q z → (v Q z Q))
3029simprd 107 . . . . . . . . . . . . . . . 16 (v <Q zz Q)
31 recclnq 6237 . . . . . . . . . . . . . . . 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 6237 . . . . . . . . . . . . . . . 16 (v Q → (*Qv) Q)
3433ad2antrr 457 . . . . . . . . . . . . . . 15 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (*Qv) Q)
35 simplr 467 . . . . . . . . . . . . . . 15 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → w Q)
36 mulcomnqg 6228 . . . . . . . . . . . . . . . 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 5581 . . . . . . . . . . . . . 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 6211 . . . . . . . . . . . . . . . . . 18 1Q Q
41 mulidnq 6234 . . . . . . . . . . . . . . . . . 18 (1Q Q → (1Q ·Q 1Q) = 1Q)
4240, 41ax-mp 7 . . . . . . . . . . . . . . . . 17 (1Q ·Q 1Q) = 1Q
43 mulcomnqg 6228 . . . . . . . . . . . . . . . . . . . . . 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 6238 . . . . . . . . . . . . . . . . . . . . 21 (v Q → (v ·Q (*Qv)) = 1Q)
4644, 45eqtr3d 2047 . . . . . . . . . . . . . . . . . . . 20 (v Q → ((*Qv) ·Q v) = 1Q)
47 recidnq 6238 . . . . . . . . . . . . . . . . . . . 20 (w Q → (w ·Q (*Qw)) = 1Q)
4846, 47oveqan12d 5443 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . 19 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → v Q)
51 mulassnqg 6229 . . . . . . . . . . . . . . . . . . . 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 6237 . . . . . . . . . . . . . . . . . . . 20 (w Q → (*Qw) Q)
5435, 53syl 14 . . . . . . . . . . . . . . . . . . 19 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (*Qw) Q)
55 mulclnq 6221 . . . . . . . . . . . . . . . . . . . 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 5596 . . . . . . . . . . . . . . . . . 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 2047 . . . . . . . . . . . . . . . . 17 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (1Q ·Q 1Q) = (((*Qv) ·Q w) ·Q (v ·Q (*Qw))))
5942, 58syl5reqr 2060 . . . . . . . . . . . . . . . 16 (((v Q w Q) (v <Q z (v ·Q (*Qw)) (2ndA))) → (((*Qv) ·Q w) ·Q (v ·Q (*Qw))) = 1Q)
60 mulclnq 6221 . . . . . . . . . . . . . . . . . . 19 (((*Qv) Q w Q) → ((*Qv) ·Q w) Q)
6133, 60sylan 267 . . . . . . . . . . . . . . . . . 18 ((v Q w Q) → ((*Qv) ·Q w) Q)
62 mulclnq 6221 . . . . . . . . . . . . . . . . . . 19 ((v Q (*Qw) Q) → (v ·Q (*Qw)) Q)
6353, 62sylan2 270 . . . . . . . . . . . . . . . . . 18 ((v Q w Q) → (v ·Q (*Qw)) Q)
64 recmulnqg 6236 . . . . . . . . . . . . . . . . . 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 2079 . . . . . . . . . . . . . 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 3731 . . . . . . . . . . . . . . . . . 18 (y = ((*Qv) ·Q w) → (((*Qz) ·Q w) <Q y ↔ ((*Qz) ·Q w) <Q ((*Qv) ·Q w)))
71 fveq2 5091 . . . . . . . . . . . . . . . . . . 19 (y = ((*Qv) ·Q w) → (*Qy) = (*Q‘((*Qv) ·Q w)))
7271eleq1d 2079 . . . . . . . . . . . . . . . . . 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 2609 . . . . . . . . . . . . . . . 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 6443 . . . . . . . . . . . . . . 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 1117 . . . . . . . . . 10 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → ((*Qz) ·Q w) (1stB))
83303ad2ant3 909 . . . . . . . . . . 11 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA)) v <Q z) → z Q)
84 mulidnq 6234 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = w)
85 mulcomnqg 6228 . . . . . . . . . . . . . . 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 2047 . . . . . . . . . . . . 13 (w Qw = (1Q ·Q w))
8887adantl 262 . . . . . . . . . . . 12 ((z Q w Q) → w = (1Q ·Q w))
89 recidnq 6238 . . . . . . . . . . . . . 14 (z Q → (z ·Q (*Qz)) = 1Q)
9089oveq1d 5439 . . . . . . . . . . . . 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 6229 . . . . . . . . . . . . . 14 ((z Q (*Qz) Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9331, 92syl3an2 1150 . . . . . . . . . . . . 13 ((z Q z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
94933anidm12 1173 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9588, 91, 943eqtr2d 2051 . . . . . . . . . . 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 5432 . . . . . . . . . . . 12 (x = ((*Qz) ·Q w) → (z ·Q x) = (z ·Q ((*Qz) ·Q w)))
9897eqeq2d 2024 . . . . . . . . . . 11 (x = ((*Qz) ·Q w) → (w = (z ·Q x) ↔ w = (z ·Q ((*Qz) ·Q w))))
9998rspcev 2624 . . . . . . . . . 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 1087 . . . . . . . 8 (((A P w <Q 1Q) (v (1stA) (v ·Q (*Qw)) (2ndA))) → (v <Q zx (1stB)w = (z ·Q x)))
102101reximdv 2389 . . . . . . 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 6453 . . . . . . . . 9 (A PB P)
104 df-imp 6309 . . . . . . . . . 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 6352 . . . . . . . . 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 2406 . . . 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 2919 1 (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 867   = wceq 1223  wex 1354   wcel 1366  {cab 1999  wrex 2276  wss 2885  cop 3342   class class class wbr 3727  cfv 4817  (class class class)co 5424  1st c1st 5676  2nd c2nd 5677  Qcnq 6126  1Qc1q 6127   ·Q cmq 6129  *Qcrq 6130   <Q cltq 6131  Pcnp 6137  1Pc1p 6138   ·P cmp 6140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-13 1377  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-coll 3835  ax-sep 3838  ax-nul 3846  ax-pow 3890  ax-pr 3907  ax-un 4108  ax-setind 4192  ax-iinf 4226
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1226  df-fal 1229  df-nf 1323  df-sb 1619  df-eu 1876  df-mo 1877  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ne 2179  df-ral 2280  df-rex 2281  df-reu 2282  df-rab 2284  df-v 2528  df-sbc 2733  df-csb 2821  df-dif 2888  df-un 2890  df-in 2892  df-ss 2899  df-nul 3193  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-int 3579  df-iun 3622  df-br 3728  df-opab 3782  df-mpt 3783  df-tr 3818  df-eprel 3989  df-id 3993  df-po 3996  df-iso 3997  df-iord 4041  df-on 4043  df-suc 4046  df-iom 4229  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-iota 4782  df-fun 4819  df-fn 4820  df-f 4821  df-f1 4822  df-fo 4823  df-f1o 4824  df-fv 4825  df-ov 5427  df-oprab 5428  df-mpt2 5429  df-1st 5678  df-2nd 5679  df-recs 5830  df-irdg 5866  df-1o 5904  df-2o 5905  df-oadd 5908  df-omul 5909  df-er 6005  df-ec 6007  df-qs 6011  df-ni 6150  df-pli 6151  df-mi 6152  df-lti 6153  df-plpq 6189  df-mpq 6190  df-enq 6192  df-nqqs 6193  df-plqqs 6194  df-mqqs 6195  df-1nqqs 6196  df-rq 6197  df-ltnqqs 6198  df-enq0 6265  df-nq0 6266  df-0nq0 6267  df-plq0 6268  df-mq0 6269  df-inp 6306  df-i1p 6307  df-imp 6309
This theorem is referenced by:  recexprlemex  6458
  Copyright terms: Public domain W3C validator