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

Theorem axcc3 8814
 Description: A possibly more useful version of ax-cc 8811 using sequences instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Mario Carneiro, 26-Dec-2014.)
Hypotheses
Ref Expression
axcc3.1
axcc3.2
Assertion
Ref Expression
axcc3
Distinct variable groups:   ,   ,,
Allowed substitution hint:   ()

Proof of Theorem axcc3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axcc3.2 . . 3
2 relen 7524 . . . 4
32brrelexi 4832 . . 3
4 mptexg 6089 . . 3
51, 3, 4mp2b 10 . 2
6 bren 7528 . . . 4
71, 6mpbi 211 . . 3
8 axcc2 8813 . . . . 5
9 f1of 5769 . . . . . . . . . . 11
10 fnfco 5703 . . . . . . . . . . 11
119, 10sylan2 476 . . . . . . . . . 10
1211adantlr 719 . . . . . . . . 9
13123adant1 1023 . . . . . . . 8
14 nfmpt1 4451 . . . . . . . . . . 11
1514nfeq2 2579 . . . . . . . . . 10
16 nfv 1755 . . . . . . . . . 10
17 nfv 1755 . . . . . . . . . 10
1815, 16, 17nf3an 1990 . . . . . . . . 9
199ffvelrnda 5976 . . . . . . . . . . . . . . . . . 18
20 fveq2 5820 . . . . . . . . . . . . . . . . . . . . 21
2120neeq1d 2655 . . . . . . . . . . . . . . . . . . . 20
22 fveq2 5820 . . . . . . . . . . . . . . . . . . . . 21
2322, 20eleq12d 2495 . . . . . . . . . . . . . . . . . . . 20
2421, 23imbi12d 321 . . . . . . . . . . . . . . . . . . 19
2524rspcv 3116 . . . . . . . . . . . . . . . . . 18
2619, 25syl 17 . . . . . . . . . . . . . . . . 17
27263ad2antl3 1169 . . . . . . . . . . . . . . . 16
28 f1ocnv 5781 . . . . . . . . . . . . . . . . . . . . . . . . 25
29 f1of 5769 . . . . . . . . . . . . . . . . . . . . . . . . 25
3028, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
31 fvco3 5897 . . . . . . . . . . . . . . . . . . . . . . . 24
3230, 31sylan 473 . . . . . . . . . . . . . . . . . . . . . . 23
3319, 32syldan 472 . . . . . . . . . . . . . . . . . . . . . 22
34333adant1 1023 . . . . . . . . . . . . . . . . . . . . 21
35 f1ocnvfv1 6129 . . . . . . . . . . . . . . . . . . . . . . 23
3635fveq2d 5824 . . . . . . . . . . . . . . . . . . . . . 22
37363adant1 1023 . . . . . . . . . . . . . . . . . . . . 21
38 fveq1 5819 . . . . . . . . . . . . . . . . . . . . . . 23
39 axcc3.1 . . . . . . . . . . . . . . . . . . . . . . . 24
40 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . 25
4140fvmpt2 5912 . . . . . . . . . . . . . . . . . . . . . . . 24
4239, 41mpan2 675 . . . . . . . . . . . . . . . . . . . . . . 23
4338, 42sylan9eq 2477 . . . . . . . . . . . . . . . . . . . . . 22
44433adant2 1024 . . . . . . . . . . . . . . . . . . . . 21
4534, 37, 443eqtrd 2461 . . . . . . . . . . . . . . . . . . . 20
46453expa 1205 . . . . . . . . . . . . . . . . . . 19
47463adantl2 1162 . . . . . . . . . . . . . . . . . 18
4847neeq1d 2655 . . . . . . . . . . . . . . . . 17
4993ad2ant3 1028 . . . . . . . . . . . . . . . . . . . 20
50 fvco3 5897 . . . . . . . . . . . . . . . . . . . 20
5149, 50sylan 473 . . . . . . . . . . . . . . . . . . 19
5251eleq1d 2485 . . . . . . . . . . . . . . . . . 18
5347eleq2d 2486 . . . . . . . . . . . . . . . . . 18
5452, 53bitr3d 258 . . . . . . . . . . . . . . . . 17
5548, 54imbi12d 321 . . . . . . . . . . . . . . . 16
5627, 55sylibd 217 . . . . . . . . . . . . . . 15
5756ex 435 . . . . . . . . . . . . . 14
5857com23 81 . . . . . . . . . . . . 13
59583exp 1204 . . . . . . . . . . . 12
6059com34 86 . . . . . . . . . . 11
6160imp32 434 . . . . . . . . . 10
62613impia 1202 . . . . . . . . 9
6318, 62ralrimi 2760 . . . . . . . 8
64 vex 3020 . . . . . . . . . 10
65 vex 3020 . . . . . . . . . 10
6664, 65coex 6698 . . . . . . . . 9
67 fneq1 5620 . . . . . . . . . 10
68 fveq1 5819 . . . . . . . . . . . . 13
6968eleq1d 2485 . . . . . . . . . . . 12
7069imbi2d 317 . . . . . . . . . . 11
7170ralbidv 2799 . . . . . . . . . 10
7267, 71anbi12d 715 . . . . . . . . 9
7366, 72spcev 3111 . . . . . . . 8
7413, 63, 73syl2anc 665 . . . . . . 7
75743exp 1204 . . . . . 6
7675exlimdv 1772 . . . . 5
778, 76mpi 20 . . . 4
7877exlimdv 1772 . . 3
797, 78mpi 20 . 2
805, 79vtocle 3093 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872   wne 2594  wral 2709  cvv 3017  c0 3699   class class class wbr 4361   cmpt 4420  ccnv 4790   ccom 4795   wfn 5534  wf 5535  wf1o 5538  cfv 5539  com 6645   cen 7516 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-inf2 8094  ax-cc 8811 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-om 6646  df-2nd 6747  df-er 7313  df-en 7520 This theorem is referenced by:  axcc4  8815  domtriomlem  8818  ovnsubaddlem2  38240
 Copyright terms: Public domain W3C validator