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

Theorem bnj1398 29380
 Description: Technical lemma for bnj60 29408. 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 3923 . . . . . . . . . 10
32bnj1436 29188 . . . . . . . . 9
41, 3bnj833 29104 . . . . . . . 8
5 bnj1398.12 . . . . . . . 8
6 bnj1398.7 . . . . . . . . . . . 12
7 nfv 1609 . . . . . . . . . . . . 13
8 nfv 1609 . . . . . . . . . . . . 13
9 nfra1 2606 . . . . . . . . . . . . 13
107, 8, 9nf3an 1786 . . . . . . . . . . . 12
116, 10nfxfr 1560 . . . . . . . . . . 11
12 nfiu1 3949 . . . . . . . . . . . 12
1312nfcri 2426 . . . . . . . . . . 11
1411, 13nfan 1783 . . . . . . . . . 10
151, 14nfxfr 1560 . . . . . . . . 9
1615nfri 1754 . . . . . . . 8
174, 5, 16bnj1521 29199 . . . . . . 7
18 bnj1398.6 . . . . . . . . . . . . . . . . . . 19
19 nfv 1609 . . . . . . . . . . . . . . . . . . . 20
20 bnj1398.5 . . . . . . . . . . . . . . . . . . . . . 22
21 nfe1 1718 . . . . . . . . . . . . . . . . . . . . . . . 24
2221nfn 1777 . . . . . . . . . . . . . . . . . . . . . . 23
23 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . 23
2422, 23nfrab 2734 . . . . . . . . . . . . . . . . . . . . . 22
2520, 24nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . 21
26 nfcv 2432 . . . . . . . . . . . . . . . . . . . . 21
2725, 26nfne 2552 . . . . . . . . . . . . . . . . . . . 20
2819, 27nfan 1783 . . . . . . . . . . . . . . . . . . 19
2918, 28nfxfr 1560 . . . . . . . . . . . . . . . . . 18
3025nfcri 2426 . . . . . . . . . . . . . . . . . 18
31 nfv 1609 . . . . . . . . . . . . . . . . . . 19
3225, 31nfral 2609 . . . . . . . . . . . . . . . . . 18
3329, 30, 32nf3an 1786 . . . . . . . . . . . . . . . . 17
346, 33nfxfr 1560 . . . . . . . . . . . . . . . 16
35 nfv 1609 . . . . . . . . . . . . . . . 16
3634, 35nfan 1783 . . . . . . . . . . . . . . 15
371, 36nfxfr 1560 . . . . . . . . . . . . . 14
38 nfv 1609 . . . . . . . . . . . . . 14
39 nfv 1609 . . . . . . . . . . . . . 14
4037, 38, 39nf3an 1786 . . . . . . . . . . . . 13
415, 40nfxfr 1560 . . . . . . . . . . . 12
4241nfri 1754 . . . . . . . . . . 11
431simplbi 446 . . . . . . . . . . . . 13
445, 43bnj835 29105 . . . . . . . . . . . 12
455simp2bi 971 . . . . . . . . . . . 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 29379 . . . . . . . . . . . . 13
52 rsp 2616 . . . . . . . . . . . . 13
5351, 52syl 15 . . . . . . . . . . . 12
5444, 45, 53sylc 56 . . . . . . . . . . 11
5542, 54bnj596 29091 . . . . . . . . . 10
5646, 47, 48, 49, 50bnj1373 29376 . . . . . . . . . . . . . 14
5756simplbi 446 . . . . . . . . . . . . 13
5857adantl 452 . . . . . . . . . . . 12
5956simprbi 450 . . . . . . . . . . . . 13
60 rspe 2617 . . . . . . . . . . . . 13
6145, 59, 60syl2an 463 . . . . . . . . . . . 12
62 bnj1398.9 . . . . . . . . . . . . . 14
6362abeq2i 2403 . . . . . . . . . . . . 13
6456rexbii 2581 . . . . . . . . . . . . 13
65 r19.42v 2707 . . . . . . . . . . . . 13
6663, 64, 653bitri 262 . . . . . . . . . . . 12
6758, 61, 66sylanbrc 645 . . . . . . . . . . 11
685simp3bi 972 . . . . . . . . . . . . 13
6968adantr 451 . . . . . . . . . . . 12
7059adantl 452 . . . . . . . . . . . 12
7169, 70eleqtrrd 2373 . . . . . . . . . . 11
7267, 71jca 518 . . . . . . . . . 10
7355, 72bnj593 29090 . . . . . . . . 9
74 df-rex 2562 . . . . . . . . 9
7573, 74sylibr 203 . . . . . . . 8
76 bnj1398.10 . . . . . . . . . . . 12
7776dmeqi 4896 . . . . . . . . . . 11
7862bnj1317 29170 . . . . . . . . . . . 12
7978bnj1400 29184 . . . . . . . . . . 11
8077, 79eqtri 2316 . . . . . . . . . 10
8180eleq2i 2360 . . . . . . . . 9
82 eliun 3925 . . . . . . . . 9
8381, 82bitri 240 . . . . . . . 8
8475, 83sylibr 203 . . . . . . 7
8517, 84bnj593 29090 . . . . . 6
86 nfre1 2612 . . . . . . . . . . . 12
8786nfab 2436 . . . . . . . . . . 11
8862, 87nfcxfr 2429 . . . . . . . . . 10
8988nfuni 3849 . . . . . . . . 9
9076, 89nfcxfr 2429 . . . . . . . 8
9190nfdm 4936 . . . . . . 7
9291nfcrii 2425 . . . . . 6
9385, 92bnj1397 29183 . . . . 5
941, 93sylbir 204 . . . 4
9594ex 423 . . 3
9695ssrdv 3198 . 2
97 simpr 447 . . . . . . . 8
9866simprbi 450 . . . . . . . . 9
9998adantr 451 . . . . . . . 8
100 r19.42v 2707 . . . . . . . . 9
101 eleq2 2357 . . . . . . . . . . 11
102101biimpac 472 . . . . . . . . . 10
103102reximi 2663 . . . . . . . . 9
104100, 103sylbir 204 . . . . . . . 8
10597, 99, 104syl2anc 642 . . . . . . 7
106105rexlimiva 2675 . . . . . 6
10783, 106sylbi 187 . . . . 5
1082abeq2i 2403 . . . . 5
109107, 108sylibr 203 . . . 4
110109ssriv 3197 . . 3
111110a1i 10 . 2
11296, 111eqssd 3209 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934  wex 1531   wceq 1632   wcel 1696  cab 2282   wne 2459  wral 2556  wrex 2557  crab 2560  wsbc 3004   cun 3163   wss 3165  c0 3468  csn 3653  cop 3656  cuni 3843  ciun 3921   class class class wbr 4039   cdm 4705   cres 4707   wfn 5266  cfv 5271   c-bnj14 29029   w-bnj15 29033   c-bnj18 29035 This theorem is referenced by:  bnj1415  29384 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-dm 4715  df-bnj14 29030  df-bnj18 29036
 Copyright terms: Public domain W3C validator