Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > indcardi | Unicode version |
Description: Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
Ref | Expression |
---|---|
indcardi.a | |
indcardi.b | |
indcardi.c | |
indcardi.d | |
indcardi.e | |
indcardi.f | |
indcardi.g |
Ref | Expression |
---|---|
indcardi |
S
, ,, , , ,Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indcardi.b | . . 3 | |
2 | domrefg 7570 | . . 3 | |
3 | 1, 2 | syl 16 | . 2 |
4 | indcardi.a | . . 3 | |
5 | cardon 8346 | . . . 4 | |
6 | 5 | a1i 11 | . . 3 |
7 | simpl1 999 | . . . . 5 | |
8 | simpr 461 | . . . . 5 | |
9 | simpr 461 | . . . . . . . . . . . . 13 | |
10 | simpl1 999 | . . . . . . . . . . . . . . . 16 | |
11 | 10, 1 | syl 16 | . . . . . . . . . . . . . . 15 |
12 | sdomdom 7563 | . . . . . . . . . . . . . . . . 17 | |
13 | 12 | adantl 466 | . . . . . . . . . . . . . . . 16 |
14 | simpl3 1001 | . . . . . . . . . . . . . . . 16 | |
15 | domtr 7588 | . . . . . . . . . . . . . . . 16 | |
16 | 13, 14, 15 | syl2anc 661 | . . . . . . . . . . . . . . 15 |
17 | numdom 8440 | . . . . . . . . . . . . . . 15 | |
18 | 11, 16, 17 | syl2anc 661 | . . . . . . . . . . . . . 14 |
19 | numdom 8440 | . . . . . . . . . . . . . . 15 | |
20 | 11, 14, 19 | syl2anc 661 | . . . . . . . . . . . . . 14 |
21 | cardsdom2 8390 | . . . . . . . . . . . . . 14 | |
22 | 18, 20, 21 | syl2anc 661 | . . . . . . . . . . . . 13 |
23 | 9, 22 | mpbird 232 | . . . . . . . . . . . 12 |
24 | id 22 | . . . . . . . . . . . . 13 | |
25 | 24 | com3l 81 | . . . . . . . . . . . 12 |
26 | 23, 16, 25 | sylc 60 | . . . . . . . . . . 11 |
27 | 26 | ex 434 | . . . . . . . . . 10 |
28 | 27 | com23 78 | . . . . . . . . 9 |
29 | 28 | alimdv 1709 | . . . . . . . 8 |
30 | 29 | 3exp 1195 | . . . . . . 7 |
31 | 30 | com34 83 | . . . . . 6 |
32 | 31 | 3imp1 1209 | . . . . 5 |
33 | indcardi.c | . . . . 5 | |
34 | 7, 8, 32, 33 | syl3anc 1228 | . . . 4 |
35 | 34 | ex 434 | . . 3 |
36 | indcardi.f | . . . . 5 | |
37 | 36 | breq1d 4462 | . . . 4 |
38 | indcardi.d | . . . 4 | |
39 | 37, 38 | imbi12d 320 | . . 3 |
40 | indcardi.g | . . . . 5 | |
41 | 40 | breq1d 4462 | . . . 4 |
42 | indcardi.e | . . . 4 | |
43 | 41, 42 | imbi12d 320 | . . 3 |
44 | 36 | fveq2d 5875 | . . 3 |
45 | 40 | fveq2d 5875 | . . 3 |
46 | 4, 6, 35, 39, 43, 44, 45 | tfisi 6693 | . 2 |
47 | 3, 46 | mpd 15 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
/\ wa 369 /\ w3a 973 A. wal 1393
= wceq 1395 e. wcel 1818 C_ wss 3475
class class class wbr 4452 con0 4883 dom cdm 5004 ` cfv 5593
cdom 7534 csdm 7535 ccrd 8337 |
This theorem is referenced by: uzindi 12091 symggen 16495 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-8 1820 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-rep 4563 ax-sep 4573 ax-nul 4581 ax-pow 4630 ax-pr 4691 ax-un 6592 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3435 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-pss 3491 df-nul 3785 df-if 3942 df-pw 4014 df-sn 4030 df-pr 4032 df-tp 4034 df-op 4036 df-uni 4250 df-int 4287 df-iun 4332 df-br 4453 df-opab 4511 df-mpt 4512 df-tr 4546 df-eprel 4796 df-id 4800 df-po 4805 df-so 4806 df-fr 4843 df-se 4844 df-we 4845 df-ord 4886 df-on 4887 df-suc 4889 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-isom 5602 df-riota 6257 df-recs 7061 df-er 7330 df-en 7537 df-dom 7538 df-sdom 7539 df-card 8341 |
Copyright terms: Public domain | W3C validator |