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 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
findcard3.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
findcard3.3 ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → 𝜑 ) → 𝜒 ) )
Assertion findcard3 ( 𝐴 ∈ Fin → 𝜏 )

Proof

Step Hyp Ref Expression
1 findcard3.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
2 findcard3.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
3 findcard3.3 ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → 𝜑 ) → 𝜒 ) )
4 isfi ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑤 ∈ ω 𝐴 ≈ 𝑤 )
5 nnon ⊢ ( 𝑤 ∈ ω → 𝑤 ∈ On )
6 eleq1w ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ ω ↔ 𝑧 ∈ ω ) )
7 breq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑧 ) )
8 7 imbi1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
9 8 albidv ⊢ ( 𝑤 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
10 6 9 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ) ↔ ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ) )
11 rspe ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
12 isfi ⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
13 11 12 sylibr ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → 𝑦 ∈ Fin )
14 19.21v ⊢ ( ∀ 𝑥 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ↔ ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
15 14 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑤 ∀ 𝑥 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ↔ ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
16 ralcom4 ⊢ ( ∀ 𝑧 ∈ 𝑤 ∀ 𝑥 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ↔ ∀ 𝑥 ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
17 15 16 bitr3i ⊢ ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ↔ ∀ 𝑥 ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
18 pssss ⊢ ( 𝑥 ⊊ 𝑦 → 𝑥 ⊆ 𝑦 )
19 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦 ) → 𝑥 ∈ Fin )
20 isfi ⊢ ( 𝑥 ∈ Fin ↔ ∃ 𝑧 ∈ ω 𝑥 ≈ 𝑧 )
21 19 20 sylib ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦 ) → ∃ 𝑧 ∈ ω 𝑥 ≈ 𝑧 )
22 13 18 21 syl2an ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ∃ 𝑧 ∈ ω 𝑥 ≈ 𝑧 )
23 ensym ⊢ ( 𝑥 ≈ 𝑧 → 𝑧 ≈ 𝑥 )
24 23 ad2antll ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑧 ≈ 𝑥 )
25 php3 ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑥 ⊊ 𝑦 ) → 𝑥 ≺ 𝑦 )
26 13 25 sylan ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → 𝑥 ≺ 𝑦 )
27 simpllr ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑦 ≈ 𝑤 )
28 sdomentr ⊢ ( ( 𝑥 ≺ 𝑦 ∧ 𝑦 ≈ 𝑤 ) → 𝑥 ≺ 𝑤 )
29 26 27 28 syl2an2r ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑥 ≺ 𝑤 )
30 ensdomtr ⊢ ( ( 𝑧 ≈ 𝑥 ∧ 𝑥 ≺ 𝑤 ) → 𝑧 ≺ 𝑤 )
31 24 29 30 syl2anc ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑧 ≺ 𝑤 )
32 nnon ⊢ ( 𝑧 ∈ ω → 𝑧 ∈ On )
33 32 ad2antrl ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑧 ∈ On )
34 5 ad3antrrr ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑤 ∈ On )
35 sdomel ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤 ) )
36 33 34 35 syl2anc ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → ( 𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤 ) )
37 31 36 mpd ⊢ ( ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) ∧ ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) ) → 𝑧 ∈ 𝑤 )
38 37 ex ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) → 𝑧 ∈ 𝑤 ) )
39 simpr ⊢ ( ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) → 𝑥 ≈ 𝑧 )
40 38 39 jca2 ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( ( 𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧 ) → ( 𝑧 ∈ 𝑤 ∧ 𝑥 ≈ 𝑧 ) ) )
41 40 reximdv2 ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( ∃ 𝑧 ∈ ω 𝑥 ≈ 𝑧 → ∃ 𝑧 ∈ 𝑤 𝑥 ≈ 𝑧 ) )
42 22 41 mpd ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ∃ 𝑧 ∈ 𝑤 𝑥 ≈ 𝑧 )
43 r19.29 ⊢ ( ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ ∃ 𝑧 ∈ 𝑤 𝑥 ≈ 𝑧 ) → ∃ 𝑧 ∈ 𝑤 ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ 𝑥 ≈ 𝑧 ) )
44 43 expcom ⊢ ( ∃ 𝑧 ∈ 𝑤 𝑥 ≈ 𝑧 → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ∃ 𝑧 ∈ 𝑤 ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ 𝑥 ≈ 𝑧 ) ) )
45 42 44 syl ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ∃ 𝑧 ∈ 𝑤 ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ 𝑥 ≈ 𝑧 ) ) )
46 ordom ⊢ Ord ω
47 ordelss ⊢ ( ( Ord ω ∧ 𝑤 ∈ ω ) → 𝑤 ⊆ ω )
48 46 47 mpan ⊢ ( 𝑤 ∈ ω → 𝑤 ⊆ ω )
49 48 ad2antrr ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → 𝑤 ⊆ ω )
50 49 sseld ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( 𝑧 ∈ 𝑤 → 𝑧 ∈ ω ) )
51 pm2.27 ⊢ ( 𝑧 ∈ ω → ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) )
52 51 impd ⊢ ( 𝑧 ∈ ω → ( ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ 𝑥 ≈ 𝑧 ) → 𝜑 ) )
53 50 52 syl6 ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( 𝑧 ∈ 𝑤 → ( ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ 𝑥 ≈ 𝑧 ) → 𝜑 ) ) )
54 53 rexlimdv ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( ∃ 𝑧 ∈ 𝑤 ( ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ∧ 𝑥 ≈ 𝑧 ) → 𝜑 ) )
55 45 54 syld ⊢ ( ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) ∧ 𝑥 ⊊ 𝑦 ) → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → 𝜑 ) )
56 55 ex ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → ( 𝑥 ⊊ 𝑦 → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → 𝜑 ) ) )
57 56 com23 ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ( 𝑥 ⊊ 𝑦 → 𝜑 ) ) )
58 57 alimdv ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → ( ∀ 𝑥 ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → 𝜑 ) ) )
59 17 58 syl5bi ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → 𝜑 ) ) )
60 13 59 3 sylsyld ⊢ ( ( 𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤 ) → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → 𝜒 ) )
61 60 impancom ⊢ ( ( 𝑤 ∈ ω ∧ ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ) → ( 𝑦 ≈ 𝑤 → 𝜒 ) )
62 61 alrimiv ⊢ ( ( 𝑤 ∈ ω ∧ ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) ) → ∀ 𝑦 ( 𝑦 ≈ 𝑤 → 𝜒 ) )
63 62 expcom ⊢ ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ( 𝑤 ∈ ω → ∀ 𝑦 ( 𝑦 ≈ 𝑤 → 𝜒 ) ) )
64 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑤 ↔ 𝑦 ≈ 𝑤 ) )
65 64 1 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑦 ≈ 𝑤 → 𝜒 ) ) )
66 65 cbvalvw ⊢ ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝑤 → 𝜒 ) )
67 63 66 syl6ibr ⊢ ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ) )
68 67 a1i ⊢ ( 𝑤 ∈ On → ( ∀ 𝑧 ∈ 𝑤 ( 𝑧 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑧 → 𝜑 ) ) → ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ) ) )
69 10 68 tfis2 ⊢ ( 𝑤 ∈ On → ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ) )
70 5 69 mpcom ⊢ ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) )
71 70 rgen ⊢ ∀ 𝑤 ∈ ω ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 )
72 r19.29 ⊢ ( ( ∀ 𝑤 ∈ ω ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ∧ ∃ 𝑤 ∈ ω 𝐴 ≈ 𝑤 ) → ∃ 𝑤 ∈ ω ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ∧ 𝐴 ≈ 𝑤 ) )
73 71 72 mpan ⊢ ( ∃ 𝑤 ∈ ω 𝐴 ≈ 𝑤 → ∃ 𝑤 ∈ ω ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ∧ 𝐴 ≈ 𝑤 ) )
74 4 73 sylbi ⊢ ( 𝐴 ∈ Fin → ∃ 𝑤 ∈ ω ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ∧ 𝐴 ≈ 𝑤 ) )
75 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤 ) )
76 75 2 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝐴 ≈ 𝑤 → 𝜏 ) ) )
77 76 spcgv ⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) → ( 𝐴 ≈ 𝑤 → 𝜏 ) ) )
78 77 impd ⊢ ( 𝐴 ∈ Fin → ( ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ∧ 𝐴 ≈ 𝑤 ) → 𝜏 ) )
79 78 rexlimdvw ⊢ ( 𝐴 ∈ Fin → ( ∃ 𝑤 ∈ ω ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ∧ 𝐴 ≈ 𝑤 ) → 𝜏 ) )
80 74 79 mpd ⊢ ( 𝐴 ∈ Fin → 𝜏 )