Metamath Proof Explorer


Theorem findcard3

Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013)

Ref Expression
Hypotheses findcard3.1 x=yφχ
findcard3.2 x=Aφτ
findcard3.3 yFinxxyφχ
Assertion findcard3 AFinτ

Proof

Step Hyp Ref Expression
1 findcard3.1 x=yφχ
2 findcard3.2 x=Aφτ
3 findcard3.3 yFinxxyφχ
4 isfi AFinwωAw
5 nnon wωwOn
6 eleq1w w=zwωzω
7 breq2 w=zxwxz
8 7 imbi1d w=zxwφxzφ
9 8 albidv w=zxxwφxxzφ
10 6 9 imbi12d w=zwωxxwφzωxxzφ
11 rspe wωywwωyw
12 isfi yFinwωyw
13 11 12 sylibr wωywyFin
14 19.21v xzωxzφzωxxzφ
15 14 ralbii zwxzωxzφzwzωxxzφ
16 ralcom4 zwxzωxzφxzwzωxzφ
17 15 16 bitr3i zwzωxxzφxzwzωxzφ
18 pssss xyxy
19 ssfi yFinxyxFin
20 isfi xFinzωxz
21 19 20 sylib yFinxyzωxz
22 13 18 21 syl2an wωywxyzωxz
23 ensym xzzx
24 23 ad2antll wωywxyzωxzzx
25 php3 yFinxyxy
26 13 25 sylan wωywxyxy
27 simpllr wωywxyzωxzyw
28 sdomentr xyywxw
29 26 27 28 syl2an2r wωywxyzωxzxw
30 ensdomtr zxxwzw
31 24 29 30 syl2anc wωywxyzωxzzw
32 nnon zωzOn
33 32 ad2antrl wωywxyzωxzzOn
34 5 ad3antrrr wωywxyzωxzwOn
35 sdomel zOnwOnzwzw
36 33 34 35 syl2anc wωywxyzωxzzwzw
37 31 36 mpd wωywxyzωxzzw
38 37 ex wωywxyzωxzzw
39 simpr zωxzxz
40 38 39 jca2 wωywxyzωxzzwxz
41 40 reximdv2 wωywxyzωxzzwxz
42 22 41 mpd wωywxyzwxz
43 r19.29 zwzωxzφzwxzzwzωxzφxz
44 43 expcom zwxzzwzωxzφzwzωxzφxz
45 42 44 syl wωywxyzwzωxzφzwzωxzφxz
46 ordom Ordω
47 ordelss Ordωwωwω
48 46 47 mpan wωwω
49 48 ad2antrr wωywxywω
50 49 sseld wωywxyzwzω
51 pm2.27 zωzωxzφxzφ
52 51 impd zωzωxzφxzφ
53 50 52 syl6 wωywxyzwzωxzφxzφ
54 53 rexlimdv wωywxyzwzωxzφxzφ
55 45 54 syld wωywxyzwzωxzφφ
56 55 ex wωywxyzwzωxzφφ
57 56 com23 wωywzwzωxzφxyφ
58 57 alimdv wωywxzwzωxzφxxyφ
59 17 58 syl5bi wωywzwzωxxzφxxyφ
60 13 59 3 sylsyld wωywzwzωxxzφχ
61 60 impancom wωzwzωxxzφywχ
62 61 alrimiv wωzwzωxxzφyywχ
63 62 expcom zwzωxxzφwωyywχ
64 breq1 x=yxwyw
65 64 1 imbi12d x=yxwφywχ
66 65 cbvalvw xxwφyywχ
67 63 66 syl6ibr zwzωxxzφwωxxwφ
68 67 a1i wOnzwzωxxzφwωxxwφ
69 10 68 tfis2 wOnwωxxwφ
70 5 69 mpcom wωxxwφ
71 70 rgen wωxxwφ
72 r19.29 wωxxwφwωAwwωxxwφAw
73 71 72 mpan wωAwwωxxwφAw
74 4 73 sylbi AFinwωxxwφAw
75 breq1 x=AxwAw
76 75 2 imbi12d x=AxwφAwτ
77 76 spcgv AFinxxwφAwτ
78 77 impd AFinxxwφAwτ
79 78 rexlimdvw AFinwωxxwφAwτ
80 74 79 mpd AFinτ