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

Theorem basqtop 18988
Description: An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypothesis
Ref Expression
qtopcmp.1
Assertion
Ref Expression
basqtop

Proof of Theorem basqtop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1ofo 5618 . . . . 5
2 qtopcmp.1 . . . . . . 7
32elqtop2 18978 . . . . . 6
42elqtop2 18978 . . . . . 6
53, 4anbi12d 695 . . . . 5
61, 5sylan2 464 . . . 4
7 simpl1l 1024 . . . . . . . . 9
8 simpl2r 1027 . . . . . . . . 9
9 simpl3r 1029 . . . . . . . . 9
10 simpl1r 1025 . . . . . . . . . . . 12
11 f1ocnv 5623 . . . . . . . . . . . 12
12 f1ofn 5612 . . . . . . . . . . . 12
1310, 11, 123syl 19 . . . . . . . . . . 11
14 simpl2l 1026 . . . . . . . . . . 11
15 inss1 3547 . . . . . . . . . . . 12
16 simpr 451 . . . . . . . . . . . 12
1715, 16sseldi 3331 . . . . . . . . . . 11
18 fnfvima 5923 . . . . . . . . . . 11
1913, 14, 17, 18syl3anc 1203 . . . . . . . . . 10
20 simpl3l 1028 . . . . . . . . . . 11
21 inss2 3548 . . . . . . . . . . . 12
2221, 16sseldi 3331 . . . . . . . . . . 11
23 fnfvima 5923 . . . . . . . . . . 11
2413, 20, 22, 23syl3anc 1203 . . . . . . . . . 10
2519, 24elind 3517 . . . . . . . . 9
26 basis2 18260 . . . . . . . . 9
277, 8, 9, 25, 26syl22anc 1204 . . . . . . . 8
2810adantr 455 . . . . . . . . . . 11
29 simp2l 999 . . . . . . . . . . . . . 14
3015, 29syl5ss 3344 . . . . . . . . . . . . 13
3130sselda 3333 . . . . . . . . . . . 12
3231adantr 455 . . . . . . . . . . 11
33 f1ocnvfv2 5952 . . . . . . . . . . 11
3428, 32, 33syl2anc 646 . . . . . . . . . 10
35 f1ofn 5612 . . . . . . . . . . . 12
3628, 35syl 16 . . . . . . . . . . 11
37 simprrr 749 . . . . . . . . . . . . 13
38 inss1 3547 . . . . . . . . . . . . 13
3937, 38syl6ss 3345 . . . . . . . . . . . 12
40 cnvimass 5161 . . . . . . . . . . . . 13
41 f1odm 5615 . . . . . . . . . . . . . 14
4228, 41syl 16 . . . . . . . . . . . . 13
4340, 42syl5sseq 3381 . . . . . . . . . . . 12
4439, 43sstrd 3343 . . . . . . . . . . 11
45 simprrl 748 . . . . . . . . . . 11
46 fnfvima 5923 . . . . . . . . . . 11
4736, 44, 45, 46syl3anc 1203 . . . . . . . . . 10
4834, 47eqeltrrd 2497 . . . . . . . . 9
49 imassrn 5152 . . . . . . . . . . . 12
5028, 1syl 16 . . . . . . . . . . . . 13
51 forn 5593 . . . . . . . . . . . . 13
5250, 51syl 16 . . . . . . . . . . . 12
5349, 52syl5sseq 3381 . . . . . . . . . . 11
54 f1of1 5610 . . . . . . . . . . . . . 14
5528, 54syl 16 . . . . . . . . . . . . 13
56 f1imacnv 5627 . . . . . . . . . . . . 13
5755, 44, 56syl2anc 646 . . . . . . . . . . . 12
58 simprl 740 . . . . . . . . . . . 12
5957, 58eqeltrd 2496 . . . . . . . . . . 11
607adantr 455 . . . . . . . . . . . 12
612elqtop2 18978 . . . . . . . . . . . 12
6260, 50, 61syl2anc 646 . . . . . . . . . . 11
6353, 59, 62mpbir2and 898 . . . . . . . . . 10
64 fnfun 5478 . . . . . . . . . . . . . 14
65 inpreima 5800 . . . . . . . . . . . . . 14
6636, 64, 653syl 19 . . . . . . . . . . . . 13
6737, 66sseqtr4d 3370 . . . . . . . . . . . 12
6836, 64syl 16 . . . . . . . . . . . . 13
6939, 40syl6ss 3345 . . . . . . . . . . . . 13
70 funimass3 5789 . . . . . . . . . . . . 13
7168, 69, 70syl2anc 646 . . . . . . . . . . . 12
7267, 71mpbird 226 . . . . . . . . . . 11
73 vex 2954 . . . . . . . . . . . . 13
7473inex1 4408 . . . . . . . . . . . 12
7574elpw2 4428 . . . . . . . . . . 11
7672, 75sylibr 206 . . . . . . . . . 10
7763, 76elind 3517 . . . . . . . . 9
78 elunii 4071 . . . . . . . . 9
7948, 77, 78syl2anc 646 . . . . . . . 8
8027, 79rexlimddv 2824 . . . . . . 7
8180ex 427 . . . . . 6
8281ssrdv 3339 . . . . 5
83823expib 1175 . . . 4
846, 83sylbid 209 . . 3
8584ralrimivv 2786 . 2
86 ovex 6086 . . 3
87 isbasisg 18256 . . 3
8886, 87ax-mp 5 . 2
8985, 88sylibr 206 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362  /\w3a 950  =wceq 1687  e.wcel 1749  A.wral 2694  E.wrex 2695   cvv 2951  i^icin 3304  C_wss 3305  ~Pcpw 3837  U.cuni 4066  `'ccnv 4810  domcdm 4811  rancrn 4812  "cima 4814  Funwfun 5384  Fnwfn 5385  -1-1->wf1 5387  -onto->wfo 5388  -1-1-onto->wf1o 5389  `cfv 5390  (class class class)co 6061   cqtop 14381   ctb 18206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-reu 2701  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-id 4607  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-qtop 14385  df-bases 18209
  Copyright terms: Public domain W3C validator