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

Theorem bnj1398 29577
 Description: Technical lemma for bnj60 29605. 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
bnj1398.1
bnj1398.2
bnj1398.3
bnj1398.4
bnj1398.5
bnj1398.6
bnj1398.7
bnj1398.8
bnj1398.9
bnj1398.10
bnj1398.11
bnj1398.12
Assertion
Ref Expression
bnj1398
Distinct variable groups:   ,,,,   ,   ,   ,   ,   ,   ,,,,   ,   ,,   ,   ,
Allowed substitution hints:   (,,,)   (,,,)   (,,,,)   (,,,)   (,,,,)   ()   (,,,)   (,,,)   (,,,)   (,,,)   ()   (,,,,)   (,,,)   (,,,,)   (,,,,)

Proof of Theorem bnj1398
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj1398.11 . . . . 5
2 df-iun 4124 . . . . . . . . . 10
32bnj1436 29385 . . . . . . . . 9
41, 3bnj833 29301 . . . . . . . 8
5 bnj1398.12 . . . . . . . 8
6 bnj1398.7 . . . . . . . . . . . 12
7 nfv 1631 . . . . . . . . . . . . 13
8 nfv 1631 . . . . . . . . . . . . 13
9 nfra1 2763 . . . . . . . . . . . . 13
107, 8, 9nf3an 1852 . . . . . . . . . . . 12
116, 10nfxfr 1580 . . . . . . . . . . 11
12 nfiu1 4151 . . . . . . . . . . . 12
1312nfcri 2573 . . . . . . . . . . 11
1411, 13nfan 1849 . . . . . . . . . 10
151, 14nfxfr 1580 . . . . . . . . 9
1615nfri 1781 . . . . . . . 8
174, 5, 16bnj1521 29396 . . . . . . 7
18 bnj1398.6 . . . . . . . . . . . . . . . . . . 19
19 nfv 1631 . . . . . . . . . . . . . . . . . . . 20
20 bnj1398.5 . . . . . . . . . . . . . . . . . . . . . 22
21 nfe1 1750 . . . . . . . . . . . . . . . . . . . . . . . 24
2221nfn 1814 . . . . . . . . . . . . . . . . . . . . . . 23
23 nfcv 2579 . . . . . . . . . . . . . . . . . . . . . . 23
2422, 23nfrab 2896 . . . . . . . . . . . . . . . . . . . . . 22
2520, 24nfcxfr 2576 . . . . . . . . . . . . . . . . . . . . 21
26 nfcv 2579 . . . . . . . . . . . . . . . . . . . . 21
2725, 26nfne 2702 . . . . . . . . . . . . . . . . . . . 20
2819, 27nfan 1849 . . . . . . . . . . . . . . . . . . 19
2918, 28nfxfr 1580 . . . . . . . . . . . . . . . . . 18
3025nfcri 2573 . . . . . . . . . . . . . . . . . 18
31 nfv 1631 . . . . . . . . . . . . . . . . . . 19
3225, 31nfral 2766 . . . . . . . . . . . . . . . . . 18
3329, 30, 32nf3an 1852 . . . . . . . . . . . . . . . . 17
346, 33nfxfr 1580 . . . . . . . . . . . . . . . 16
35 nfv 1631 . . . . . . . . . . . . . . . 16
3634, 35nfan 1849 . . . . . . . . . . . . . . 15
371, 36nfxfr 1580 . . . . . . . . . . . . . 14
38 nfv 1631 . . . . . . . . . . . . . 14
39 nfv 1631 . . . . . . . . . . . . . 14
4037, 38, 39nf3an 1852 . . . . . . . . . . . . 13
415, 40nfxfr 1580 . . . . . . . . . . . 12
4241nfri 1781 . . . . . . . . . . 11
431simplbi 448 . . . . . . . . . . . . 13
445, 43bnj835 29302 . . . . . . . . . . . 12
455simp2bi 974 . . . . . . . . . . . 12
46 bnj1398.1 . . . . . . . . . . . . . 14
47 bnj1398.2 . . . . . . . . . . . . . 14
48 bnj1398.3 . . . . . . . . . . . . . 14
49 bnj1398.4 . . . . . . . . . . . . . 14
50 bnj1398.8 . . . . . . . . . . . . . 14
5146, 47, 48, 49, 20, 18, 6, 50bnj1388 29576 . . . . . . . . . . . . 13
52 rsp 2773 . . . . . . . . . . . . 13
5351, 52syl 16 . . . . . . . . . . . 12
5444, 45, 53sylc 59 . . . . . . . . . . 11
5542, 54bnj596 29288 . . . . . . . . . 10
5646, 47, 48, 49, 50bnj1373 29573 . . . . . . . . . . . . . 14
5756simplbi 448 . . . . . . . . . . . . 13
5857adantl 454 . . . . . . . . . . . 12
5956simprbi 452 . . . . . . . . . . . . 13
60 rspe 2774 . . . . . . . . . . . . 13
6145, 59, 60syl2an 465 . . . . . . . . . . . 12
62 bnj1398.9 . . . . . . . . . . . . . 14
6362abeq2i 2550 . . . . . . . . . . . . 13
6456rexbii 2737 . . . . . . . . . . . . 13
65 r19.42v 2869 . . . . . . . . . . . . 13
6663, 64, 653bitri 264 . . . . . . . . . . . 12
6758, 61, 66sylanbrc 647 . . . . . . . . . . 11
685simp3bi 975 . . . . . . . . . . . . 13
6968adantr 453 . . . . . . . . . . . 12
7059adantl 454 . . . . . . . . . . . 12
7169, 70eleqtrrd 2520 . . . . . . . . . . 11
7267, 71jca 520 . . . . . . . . . 10
7355, 72bnj593 29287 . . . . . . . . 9
74 df-rex 2718 . . . . . . . . 9
7573, 74sylibr 205 . . . . . . . 8
76 bnj1398.10 . . . . . . . . . . . 12
7776dmeqi 5106 . . . . . . . . . . 11
7862bnj1317 29367 . . . . . . . . . . . 12
7978bnj1400 29381 . . . . . . . . . . 11
8077, 79eqtri 2463 . . . . . . . . . 10
8180eleq2i 2507 . . . . . . . . 9
82 eliun 4126 . . . . . . . . 9
8381, 82bitri 242 . . . . . . . 8
8475, 83sylibr 205 . . . . . . 7
8517, 84bnj593 29287 . . . . . 6
86 nfre1 2769 . . . . . . . . . . . 12
8786nfab 2583 . . . . . . . . . . 11
8862, 87nfcxfr 2576 . . . . . . . . . 10
8988nfuni 4050 . . . . . . . . 9
9076, 89nfcxfr 2576 . . . . . . . 8
9190nfdm 5146 . . . . . . 7
9291nfcrii 2572 . . . . . 6
9385, 92bnj1397 29380 . . . . 5
941, 93sylbir 206 . . . 4
9594ex 425 . . 3
9695ssrdv 3343 . 2
97 simpr 449 . . . . . . 7
9866simprbi 452 . . . . . . . 8
9998adantr 453 . . . . . . 7
100 r19.42v 2869 . . . . . . . 8
101 eleq2 2504 . . . . . . . . . 10
102101biimpac 474 . . . . . . . . 9
103102reximi 2820 . . . . . . . 8
104100, 103sylbir 206 . . . . . . 7
10597, 99, 104syl2anc 644 . . . . . 6
106105rexlimiva 2832 . . . . 5
107 eliun 4126 . . . . 5
108106, 83, 1073imtr4i 259 . . . 4
109108ssriv 3341 . . 3
110109a1i 11 . 2
11196, 110eqssd 3354 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937  wex 1551   wceq 1654   wcel 1728  cab 2429   wne 2606  wral 2712  wrex 2713  crab 2716  wsbc 3170   cun 3307   wss 3309  c0 3616  csn 3843  cop 3846  cuni 4044  ciun 4122   class class class wbr 4243   cdm 4913   cres 4915   wfn 5484  cfv 5489   c-bnj14 29226   w-bnj15 29230   c-bnj18 29232 This theorem is referenced by:  bnj1415  29581 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-iun 4124  df-br 4244  df-dm 4923  df-bnj14 29227  df-bnj18 29233
 Copyright terms: Public domain W3C validator