ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcanprlemu Unicode version
Theorem addcanprlemu 7972
Description: Lemma for addcanprg 7973. (Contributed by Jim Kingdon, 25-Dec-2019.)
Assertion
Ref Expression
addcanprlemu |- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) -> ( 2nd ` B ) C_ ( 2nd ` C ) )
Proof of Theorem addcanprlemu
Dummy variables f g h q r s t u v w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 7832 . . . . . . 7 |- ( B e. P. -> <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. )
2 prnminu 7846 . . . . . . 7 |- ( ( <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. /\ v e. ( 2nd ` B ) ) -> E. r e. ( 2nd ` B ) r <Q v )
31, 2sylan 283 . . . . . 6 |- ( ( B e. P. /\ v e. ( 2nd ` B ) ) -> E. r e. ( 2nd ` B ) r <Q v )
433ad2antl2 1191 . . . . 5 |- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ v e. ( 2nd ` B ) ) -> E. r e. ( 2nd ` B ) r <Q v )
54adantlr 481 . . . 4 |- ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) -> E. r e. ( 2nd ` B ) r <Q v )
6 simprr 537 . . . . . 6 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) -> r <Q v )
7 ltexnqi 7766 . . . . . 6 |- ( r <Q v -> E. w e. Q. ( r +Q w ) = v )
86, 7syl 14 . . . . 5 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) -> E. w e. Q. ( r +Q w ) = v )
9 simprl 535 . . . . . . 7 |- ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) -> w e. Q. )
10 halfnqq 7767 . . . . . . 7 |- ( w e. Q. -> E. t e. Q. ( t +Q t ) = w )
119, 10syl 14 . . . . . 6 |- ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) -> E. t e. Q. ( t +Q t ) = w )
12 prop 7832 . . . . . . . . . . . . . 14 |- ( A e. P. -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. )
13 prarloc2 7861 . . . . . . . . . . . . . 14 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ t e. Q. ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
1412, 13sylan 283 . . . . . . . . . . . . 13 |- ( ( A e. P. /\ t e. Q. ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
1514adantrr 483 . . . . . . . . . . . 12 |- ( ( A e. P. /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
16153ad2antl1 1190 . . . . . . . . . . 11 |- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
1716adantlr 481 . . . . . . . . . 10 |- ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
1817adantlr 481 . . . . . . . . 9 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
1918adantlr 481 . . . . . . . 8 |- ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
2019adantlr 481 . . . . . . 7 |- ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> E. u e. ( 1st ` A ) ( u +Q t ) e. ( 2nd ` A ) )
21 simplll 539 . . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) -> ( A e. P. /\ B e. P. /\ C e. P. ) )
2221ad3antrrr 496 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( A e. P. /\ B e. P. /\ C e. P. ) )
2322simp1d 1040 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> A e. P. )
2422simp2d 1041 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> B e. P. )
25 addclpr 7894 . . . . . . . . . . . 12 |- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )
2623, 24, 25syl2anc 415 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( A +P. B ) e. P. )
27 prop 7832 . . . . . . . . . . 11 |- ( ( A +P. B ) e. P. -> <. ( 1st ` ( A +P. B ) ) , ( 2nd ` ( A +P. B ) ) >. e. P. )
2826, 27syl 14 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> <. ( 1st ` ( A +P. B ) ) , ( 2nd ` ( A +P. B ) ) >. e. P. )
2923, 12syl 14 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. )
30 simprl 535 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> u e. ( 1st ` A ) )
31 elprnql 7838 . . . . . . . . . . . . 13 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ u e. ( 1st ` A ) ) -> u e. Q. )
3229, 30, 31syl2anc 415 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> u e. Q. )
33 simplrl 541 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> t e. Q. )
34 addclnq 7732 . . . . . . . . . . . 12 |- ( ( u e. Q. /\ t e. Q. ) -> ( u +Q t ) e. Q. )
3532, 33, 34syl2anc 415 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( u +Q t ) e. Q. )
3624, 1syl 14 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. )
37 simprl 535 . . . . . . . . . . . . 13 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) -> r e. ( 2nd ` B ) )
3837ad3antrrr 496 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> r e. ( 2nd ` B ) )
39 elprnqu 7839 . . . . . . . . . . . 12 |- ( ( <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. /\ r e. ( 2nd ` B ) ) -> r e. Q. )
4036, 38, 39syl2anc 415 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> r e. Q. )
41 addclnq 7732 . . . . . . . . . . 11 |- ( ( ( u +Q t ) e. Q. /\ r e. Q. ) -> ( ( u +Q t ) +Q r ) e. Q. )
4235, 40, 41syl2anc 415 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) e. Q. )
43 prdisj 7849 . . . . . . . . . 10 |- ( ( <. ( 1st ` ( A +P. B ) ) , ( 2nd ` ( A +P. B ) ) >. e. P. /\ ( ( u +Q t ) +Q r ) e. Q. ) -> -. ( ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. B ) ) /\ ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
4428, 42, 43syl2anc 415 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> -. ( ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. B ) ) /\ ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
45 addassnqg 7739 . . . . . . . . . . . . . . 15 |- ( ( u e. Q. /\ t e. Q. /\ r e. Q. ) -> ( ( u +Q t ) +Q r ) = ( u +Q ( t +Q r ) ) )
4632, 33, 40, 45syl3anc 1278 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) = ( u +Q ( t +Q r ) ) )
47 addcomnqg 7738 . . . . . . . . . . . . . . . 16 |- ( ( t e. Q. /\ r e. Q. ) -> ( t +Q r ) = ( r +Q t ) )
4847oveq2d 6091 . . . . . . . . . . . . . . 15 |- ( ( t e. Q. /\ r e. Q. ) -> ( u +Q ( t +Q r ) ) = ( u +Q ( r +Q t ) ) )
4933, 40, 48syl2anc 415 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( u +Q ( t +Q r ) ) = ( u +Q ( r +Q t ) ) )
5046, 49eqtrd 2271 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) = ( u +Q ( r +Q t ) ) )
5150adantr 276 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( u +Q t ) +Q r ) = ( u +Q ( r +Q t ) ) )
52 simplrl 541 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> u e. ( 1st ` A ) )
53 simpr 110 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( r +Q t ) e. ( 1st ` C ) )
5423adantr 276 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> A e. P. )
5522simp3d 1042 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> C e. P. )
5655adantr 276 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> C e. P. )
57 df-iplp 7825 . . . . . . . . . . . . . . 15 |- +P. = ( q e. P. , s e. P. |-> <. { f e. Q. | E. g e. Q. E. h e. Q. ( g e. ( 1st ` q ) /\ h e. ( 1st ` s ) /\ f = ( g +Q h ) ) } , { f e. Q. | E. g e. Q. E. h e. Q. ( g e. ( 2nd ` q ) /\ h e. ( 2nd ` s ) /\ f = ( g +Q h ) ) } >. )
58 addclnq 7732 . . . . . . . . . . . . . . 15 |- ( ( g e. Q. /\ h e. Q. ) -> ( g +Q h ) e. Q. )
5957, 58genpprecll 7871 . . . . . . . . . . . . . 14 |- ( ( A e. P. /\ C e. P. ) -> ( ( u e. ( 1st ` A ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( u +Q ( r +Q t ) ) e. ( 1st ` ( A +P. C ) ) ) )
6054, 56, 59syl2anc 415 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( u e. ( 1st ` A ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( u +Q ( r +Q t ) ) e. ( 1st ` ( A +P. C ) ) ) )
6152, 53, 60mp2and 437 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( u +Q ( r +Q t ) ) e. ( 1st ` ( A +P. C ) ) )
6251, 61eqeltrd 2315 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. C ) ) )
63 fveq2 5690 . . . . . . . . . . . . 13 |- ( ( A +P. B ) = ( A +P. C ) -> ( 1st ` ( A +P. B ) ) = ( 1st ` ( A +P. C ) ) )
6463eleq2d 2308 . . . . . . . . . . . 12 |- ( ( A +P. B ) = ( A +P. C ) -> ( ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. B ) ) <-> ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. C ) ) ) )
6564ad7antlr 505 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. B ) ) <-> ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. C ) ) ) )
6662, 65mpbird 167 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. B ) ) )
6757, 58genppreclu 7872 . . . . . . . . . . . . . . . . . . 19 |- ( ( A e. P. /\ B e. P. ) -> ( ( ( u +Q t ) e. ( 2nd ` A ) /\ r e. ( 2nd ` B ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
6867ancomsd 269 . . . . . . . . . . . . . . . . . 18 |- ( ( A e. P. /\ B e. P. ) -> ( ( r e. ( 2nd ` B ) /\ ( u +Q t ) e. ( 2nd ` A ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
69683adant3 1048 . . . . . . . . . . . . . . . . 17 |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( r e. ( 2nd ` B ) /\ ( u +Q t ) e. ( 2nd ` A ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
7069ad2antrr 492 . . . . . . . . . . . . . . . 16 |- ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) -> ( ( r e. ( 2nd ` B ) /\ ( u +Q t ) e. ( 2nd ` A ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
7170imp 124 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) )
7271adantrlr 489 . . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( ( r e. ( 2nd ` B ) /\ r <Q v ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) )
7372anassrs 404 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( u +Q t ) e. ( 2nd ` A ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) )
7473ad2ant2rl 515 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) )
7574adantlr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) )
7675adantr 276 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) )
7766, 76jca 306 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) /\ ( r +Q t ) e. ( 1st ` C ) ) -> ( ( ( u +Q t ) +Q r ) e. ( 1st ` ( A +P. B ) ) /\ ( ( u +Q t ) +Q r ) e. ( 2nd ` ( A +P. B ) ) ) )
7844, 77mtand 675 . . . . . . . 8 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> -. ( r +Q t ) e. ( 1st ` C ) )
79 prop 7832 . . . . . . . . . . 11 |- ( C e. P. -> <. ( 1st ` C ) , ( 2nd ` C ) >. e. P. )
8055, 79syl 14 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> <. ( 1st ` C ) , ( 2nd ` C ) >. e. P. )
81 ltaddnq 7764 . . . . . . . . . . . . . 14 |- ( ( t e. Q. /\ t e. Q. ) -> t <Q ( t +Q t ) )
8233, 33, 81syl2anc 415 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> t <Q ( t +Q t ) )
83 simplrr 542 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( t +Q t ) = w )
8482, 83breqtrd 4151 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> t <Q w )
85 ltanqi 7759 . . . . . . . . . . . 12 |- ( ( t <Q w /\ r e. Q. ) -> ( r +Q t ) <Q ( r +Q w ) )
8684, 40, 85syl2anc 415 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( r +Q t ) <Q ( r +Q w ) )
87 simprr 537 . . . . . . . . . . . 12 |- ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) -> ( r +Q w ) = v )
8887ad2antrr 492 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( r +Q w ) = v )
8986, 88breqtrd 4151 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( r +Q t ) <Q v )
90 prloc 7848 . . . . . . . . . 10 |- ( ( <. ( 1st ` C ) , ( 2nd ` C ) >. e. P. /\ ( r +Q t ) <Q v ) -> ( ( r +Q t ) e. ( 1st ` C ) \/ v e. ( 2nd ` C ) ) )
9180, 89, 90syl2anc 415 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( ( r +Q t ) e. ( 1st ` C ) \/ v e. ( 2nd ` C ) ) )
9291orcomd 741 . . . . . . . 8 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> ( v e. ( 2nd ` C ) \/ ( r +Q t ) e. ( 1st ` C ) ) )
9378, 92ecased 1390 . . . . . . 7 |- ( ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) /\ ( u e. ( 1st ` A ) /\ ( u +Q t ) e. ( 2nd ` A ) ) ) -> v e. ( 2nd ` C ) )
9420, 93rexlimddv 2673 . . . . . 6 |- ( ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) /\ ( t e. Q. /\ ( t +Q t ) = w ) ) -> v e. ( 2nd ` C ) )
9511, 94rexlimddv 2673 . . . . 5 |- ( ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) /\ ( w e. Q. /\ ( r +Q w ) = v ) ) -> v e. ( 2nd ` C ) )
968, 95rexlimddv 2673 . . . 4 |- ( ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) /\ ( r e. ( 2nd ` B ) /\ r <Q v ) ) -> v e. ( 2nd ` C ) )
975, 96rexlimddv 2673 . . 3 |- ( ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) /\ v e. ( 2nd ` B ) ) -> v e. ( 2nd ` C ) )
9897ex 115 . 2 |- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) -> ( v e. ( 2nd ` B ) -> v e. ( 2nd ` C ) ) )
9998ssrdv 3254 1 |- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) -> ( 2nd ` B ) C_ ( 2nd ` C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720   /\ w3a 1009   = wceq 1402   e. wcel 2209   E.wrex 2529   C_ wss 3220   <.cop 3708   class class class wbr 4125   ` cfv 5372  (class class class)co 6075   1stc1st 6362   2ndc2nd 6363   Q.cnq 7637   +Q cplq 7639   <Q cltq 7642   P.cnp 7648   +P. cpp 7650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4241  ax-sep 4244  ax-nul 4254  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-iinf 4730
This theorem depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-tr 4225  df-eprel 4429  df-id 4433  df-po 4436  df-iso 4437  df-iord 4506  df-on 4508  df-suc 4511  df-iom 4733  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-ov 6078  df-oprab 6079  df-mpo 6080  df-1st 6364  df-2nd 6365  df-recs 6566  df-irdg 6631  df-1o 6677  df-2o 6678  df-oadd 6681  df-omul 6682  df-er 6797  df-ec 6799  df-qs 6803  df-ni 7661  df-pli 7662  df-mi 7663  df-lti 7664  df-plpq 7701  df-mpq 7702  df-enq 7704  df-nqqs 7705  df-plqqs 7706  df-mqqs 7707  df-1nqqs 7708  df-rq 7709  df-ltnqqs 7710  df-enq0 7781  df-nq0 7782  df-0nq0 7783  df-plq0 7784  df-mq0 7785  df-inp 7823  df-iplp 7825
This theorem is referenced by:  addcanprg  7973
  Copyright terms: Public domain W3C validator