Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isf34lem5 Structured version   Visualization version   Unicode version

Theorem isf34lem5 8805
 Description: Lemma for isfin3-4 8809. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Hypothesis
Ref Expression
compss.a
Assertion
Ref Expression
isf34lem5
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem isf34lem5
StepHypRef Expression
1 imassrn 5178 . . . . . . 7
2 compss.a . . . . . . . . . 10
32isf34lem2 8800 . . . . . . . . 9
43adantr 467 . . . . . . . 8
5 frn 5733 . . . . . . . 8
64, 5syl 17 . . . . . . 7
71, 6syl5ss 3442 . . . . . 6
8 simprl 763 . . . . . . . . . 10
9 fdm 5731 . . . . . . . . . . 11
104, 9syl 17 . . . . . . . . . 10
118, 10sseqtr4d 3468 . . . . . . . . 9
12 dfss1 3636 . . . . . . . . 9
1311, 12sylib 200 . . . . . . . 8
14 simprr 765 . . . . . . . 8
1513, 14eqnetrd 2690 . . . . . . 7
16 imadisj 5186 . . . . . . . 8
1716necon3bii 2675 . . . . . . 7
1815, 17sylibr 216 . . . . . 6
197, 18jca 535 . . . . 5
202isf34lem4 8804 . . . . 5
2119, 20syldan 473 . . . 4
222isf34lem3 8802 . . . . . 6
2322adantrr 722 . . . . 5
2423inteqd 4238 . . . 4
2521, 24eqtrd 2484 . . 3
2625fveq2d 5867 . 2
272compsscnv 8798 . . . 4
2827fveq1i 5864 . . 3
292compssiso 8801 . . . . . 6 [] []
30 isof1o 6214 . . . . . 6 [] []
3129, 30syl 17 . . . . 5
3231adantr 467 . . . 4
33 sspwuni 4366 . . . . . 6
347, 33sylib 200 . . . . 5
35 elpw2g 4565 . . . . . 6
3635adantr 467 . . . . 5
3734, 36mpbird 236 . . . 4
38 f1ocnvfv1 6173 . . . 4
3932, 37, 38syl2anc 666 . . 3
4028, 39syl5eqr 2498 . 2
4126, 40eqtr3d 2486 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1443   wcel 1886   wne 2621   cdif 3400   cin 3402   wss 3403  c0 3730  cpw 3950  cuni 4197  cint 4233   cmpt 4460  ccnv 4832   cdm 4833   crn 4834  cima 4836  wf 5577  wf1o 5580  cfv 5581   wiso 5582   [] crpss 6567 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-int 4234  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-rpss 6568 This theorem is referenced by:  isf34lem7  8806
 Copyright terms: Public domain W3C validator