Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1450 Structured version   Visualization version   Unicode version

Theorem bnj1450 29931
 Description: Technical lemma for bnj60 29943. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1450.1
bnj1450.2
bnj1450.3
bnj1450.4
bnj1450.5
bnj1450.6
bnj1450.7
bnj1450.8
bnj1450.9
bnj1450.10
bnj1450.11
bnj1450.12
bnj1450.13
bnj1450.14
bnj1450.15
bnj1450.16
bnj1450.17
bnj1450.18
bnj1450.19
bnj1450.20
bnj1450.21
bnj1450.22
bnj1450.23
Assertion
Ref Expression
bnj1450
Distinct variable groups:   ,,,,,   ,   ,   ,,,   ,,,,,   ,,,,,   ,   ,   ,
Allowed substitution hints:   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,)   (,,,,)   (,,,,)   (,,,)   (,,,)   (,,,,)   (,,,,)

Proof of Theorem bnj1450
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj1450.19 . . . . . . . . 9
21simprbi 471 . . . . . . . 8
3 bnj1450.17 . . . . . . . . . 10
4 bnj1450.15 . . . . . . . . . . 11
5 fndm 5685 . . . . . . . . . . 11
64, 5syl 17 . . . . . . . . . 10
73, 6bnj832 29640 . . . . . . . . 9
81, 7bnj832 29640 . . . . . . . 8
92, 8eleqtrrd 2552 . . . . . . 7
10 bnj1450.10 . . . . . . . 8
1110dmeqi 5041 . . . . . . 7
129, 11syl6eleq 2559 . . . . . 6
13 bnj1450.9 . . . . . . . 8
1413bnj1317 29705 . . . . . . 7
1514bnj1400 29719 . . . . . 6
1612, 15syl6eleq 2559 . . . . 5
1716bnj1405 29720 . . . 4
18 bnj1450.20 . . . 4
19 bnj1450.1 . . . . 5
20 bnj1450.2 . . . . 5
21 bnj1450.3 . . . . 5
22 bnj1450.4 . . . . 5
23 bnj1450.5 . . . . 5
24 bnj1450.6 . . . . 5
25 bnj1450.7 . . . . 5
26 bnj1450.8 . . . . 5
27 bnj1450.11 . . . . 5
28 bnj1450.12 . . . . 5
29 bnj1450.13 . . . . 5
30 bnj1450.14 . . . . 5
31 bnj1450.16 . . . . 5
32 bnj1450.18 . . . . 5
3319, 20, 21, 22, 23, 24, 25, 26, 13, 10, 27, 28, 29, 30, 4, 31, 3, 32, 1bnj1449 29929 . . . 4
3417, 18, 33bnj1521 29734 . . 3
3513bnj1436 29723 . . . . . . . . . 10
3618, 35bnj836 29643 . . . . . . . . 9
3719, 20, 21, 22, 26bnj1373 29911 . . . . . . . . . 10
3837rexbii 2881 . . . . . . . . 9
3936, 38sylib 201 . . . . . . . 8
4039bnj1196 29678 . . . . . . 7
41 3anass 1011 . . . . . . 7
4240, 41bnj1198 29679 . . . . . 6
43 bnj1450.21 . . . . . . 7
44 bnj252 29580 . . . . . . 7
4543, 44bitri 257 . . . . . 6
4619, 20, 21, 22, 23, 24, 25, 26, 13, 10, 27, 28, 29, 30, 4, 31, 3, 32, 1, 18bnj1444 29924 . . . . . 6
4742, 45, 46bnj1340 29707 . . . . 5
4821bnj1436 29723 . . . . . . . . . . 11
4943, 48bnj771 29647 . . . . . . . . . 10
5049bnj1196 29678 . . . . . . . . 9
51 3anass 1011 . . . . . . . . 9
5250, 51bnj1198 29679 . . . . . . . 8
53 bnj1450.22 . . . . . . . . 9
54 bnj252 29580 . . . . . . . . 9
5553, 54bitri 257 . . . . . . . 8
56 bnj1450.23 . . . . . . . . 9
5719, 20, 21, 22, 23, 24, 25, 26, 13, 10, 27, 28, 29, 30, 4, 31, 3, 32, 1, 18, 43, 53, 56bnj1445 29925 . . . . . . . 8
5852, 55, 57bnj1340 29707 . . . . . . 7
5953bnj1254 29693 . . . . . . . . . 10
60 fveq2 5879 . . . . . . . . . . . 12
61 id 22 . . . . . . . . . . . . . . 15
62 bnj602 29798 . . . . . . . . . . . . . . . 16
6362reseq2d 5111 . . . . . . . . . . . . . . 15
6461, 63opeq12d 4166 . . . . . . . . . . . . . 14
6564, 20, 563eqtr4g 2530 . . . . . . . . . . . . 13
6665fveq2d 5883 . . . . . . . . . . . 12
6760, 66eqeq12d 2486 . . . . . . . . . . 11
6867cbvralv 3005 . . . . . . . . . 10
6959, 68sylib 201 . . . . . . . . 9
7018simp3bi 1047 . . . . . . . . . . . 12
7143, 70bnj769 29645 . . . . . . . . . . 11
7253, 71bnj769 29645 . . . . . . . . . 10
73 fndm 5685 . . . . . . . . . . 11
7453, 73bnj771 29647 . . . . . . . . . 10
7572, 74eleqtrd 2551 . . . . . . . . 9
7669, 75bnj1294 29701 . . . . . . . 8
7731bnj930 29653 . . . . . . . . . . . . . 14
783, 77bnj832 29640 . . . . . . . . . . . . 13
791, 78bnj832 29640 . . . . . . . . . . . 12
8018, 79bnj835 29642 . . . . . . . . . . 11
8143, 80bnj769 29645 . . . . . . . . . 10
8253, 81bnj769 29645 . . . . . . . . 9
8318simp2bi 1046 . . . . . . . . . . . 12
8443, 83bnj769 29645 . . . . . . . . . . 11
8553, 84bnj769 29645 . . . . . . . . . 10
86 elssuni 4219 . . . . . . . . . . 11
8786, 10syl6sseqr 3465 . . . . . . . . . 10
88 ssun3 3590 . . . . . . . . . . 11
8988, 28syl6sseqr 3465 . . . . . . . . . 10
9085, 87, 893syl 18 . . . . . . . . 9
9182, 90, 72bnj1502 29731 . . . . . . . 8
9219bnj1517 29733 . . . . . . . . . . . . . . . 16
9353, 92bnj770 29646 . . . . . . . . . . . . . . 15
9462sseq1d 3445 . . . . . . . . . . . . . . . 16
9594cbvralv 3005 . . . . . . . . . . . . . . 15
9693, 95sylib 201 . . . . . . . . . . . . . 14
9796, 75bnj1294 29701 . . . . . . . . . . . . 13
9897, 74sseqtr4d 3455 . . . . . . . . . . . 12
9982, 90, 98bnj1503 29732 . . . . . . . . . . 11
10099opeq2d 4165 . . . . . . . . . 10
101100, 29, 563eqtr4g 2530 . . . . . . . . 9
102101fveq2d 5883 . . . . . . . 8
10376, 91, 1023eqtr4d 2515 . . . . . . 7
10458, 103bnj593 29627 . . . . . 6
10519, 20, 21, 22, 23, 24, 25, 26, 13, 10, 27, 28, 29bnj1446 29926 . . . . . 6
106104, 105bnj1397 29718 . . . . 5
10747, 106bnj593 29627 . . . 4
10819, 20, 21, 22, 23, 24, 25, 26, 13, 10, 27, 28, 29bnj1447 29927 . . . 4
109107, 108bnj1397 29718 . . 3
11034, 109bnj593 29627 . 2
11119, 20, 21, 22, 23, 24, 25, 26, 13, 10, 27, 28, 29bnj1448 29928 . 2
112110, 111bnj1397 29718 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904  cab 2457   wne 2641  wral 2756  wrex 2757  crab 2760  wsbc 3255   cun 3388   wss 3390  c0 3722  csn 3959  cop 3965  cuni 4190  ciun 4269   class class class wbr 4395   cdm 4839   cres 4841   wfun 5583   wfn 5584  cfv 5589   w-bnj17 29563   c-bnj14 29565   w-bnj15 29569   c-bnj18 29571 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-res 4851  df-iota 5553  df-fun 5591  df-fn 5592  df-fv 5597  df-bnj17 29564  df-bnj14 29566  df-bnj18 29572 This theorem is referenced by:  bnj1423  29932
 Copyright terms: Public domain W3C validator