This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem findcard

Description: Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses findcard.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
findcard.2 ⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( 𝜑 ↔ 𝜒 ) )
findcard.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
findcard.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
findcard.5 ⊢ 𝜓
findcard.6 ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑧 ∈ 𝑦 𝜒 → 𝜃 ) )
Assertion findcard ( 𝐴 ∈ Fin → 𝜏 )

Proof

Step Hyp Ref Expression
1 findcard.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2 findcard.2 ⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( 𝜑 ↔ 𝜒 ) )
3 findcard.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4 findcard.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 findcard.5 ⊢ 𝜓
6 findcard.6 ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑧 ∈ 𝑦 𝜒 → 𝜃 ) )
7 isfi ⊢ ( 𝑥 ∈ Fin ↔ ∃ 𝑤 ∈ ω 𝑥 ≈ 𝑤 )
8 breq2 ⊢ ( 𝑤 = ∅ → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅ ) )
9 8 imbi1d ⊢ ( 𝑤 = ∅ → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ ∅ → 𝜑 ) ) )
10 9 albidv ⊢ ( 𝑤 = ∅ → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ ∅ → 𝜑 ) ) )
11 breq2 ⊢ ( 𝑤 = 𝑣 → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣 ) )
12 11 imbi1d ⊢ ( 𝑤 = 𝑣 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ 𝑣 → 𝜑 ) ) )
13 12 albidv ⊢ ( 𝑤 = 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ) )
14 breq2 ⊢ ( 𝑤 = suc 𝑣 → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣 ) )
15 14 imbi1d ⊢ ( 𝑤 = suc 𝑣 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
16 15 albidv ⊢ ( 𝑤 = suc 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
17 en0 ⊢ ( 𝑥 ≈ ∅ ↔ 𝑥 = ∅ )
18 5 1 mpbiri ⊢ ( 𝑥 = ∅ → 𝜑 )
19 17 18 sylbi ⊢ ( 𝑥 ≈ ∅ → 𝜑 )
20 19 ax-gen ⊢ ∀ 𝑥 ( 𝑥 ≈ ∅ → 𝜑 )
21 peano2 ⊢ ( 𝑣 ∈ ω → suc 𝑣 ∈ ω )
22 breq2 ⊢ ( 𝑤 = suc 𝑣 → ( 𝑦 ≈ 𝑤 ↔ 𝑦 ≈ suc 𝑣 ) )
23 22 rspcev ⊢ ( ( suc 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
24 21 23 sylan ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
25 isfi ⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
26 24 25 sylibr ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → 𝑦 ∈ Fin )
27 26 3adant2 ⊢ ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ∧ 𝑦 ≈ suc 𝑣 ) → 𝑦 ∈ Fin )
28 dif1ennn ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑦 ) → ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 )
29 28 3expa ⊢ ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 )
30 vex ⊢ 𝑦 ∈ V
31 30 difexi ⊢ ( 𝑦 ∖ { 𝑧 } ) ∈ V
32 breq1 ⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( 𝑥 ≈ 𝑣 ↔ ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 ) )
33 32 2 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( ( 𝑥 ≈ 𝑣 → 𝜑 ) ↔ ( ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 → 𝜒 ) ) )
34 31 33 spcv ⊢ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 → 𝜒 ) )
35 29 34 syl5com ⊢ ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) ∧ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → 𝜒 ) )
36 35 ralrimdva ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑧 ∈ 𝑦 𝜒 ) )
37 36 imp ⊢ ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ) → ∀ 𝑧 ∈ 𝑦 𝜒 )
38 37 an32s ⊢ ( ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ) ∧ 𝑦 ≈ suc 𝑣 ) → ∀ 𝑧 ∈ 𝑦 𝜒 )
39 38 3impa ⊢ ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ∧ 𝑦 ≈ suc 𝑣 ) → ∀ 𝑧 ∈ 𝑦 𝜒 )
40 27 39 6 sylc ⊢ ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ∧ 𝑦 ≈ suc 𝑣 ) → 𝜃 )
41 40 3exp ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( 𝑦 ≈ suc 𝑣 → 𝜃 ) ) )
42 41 alrimdv ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑦 ( 𝑦 ≈ suc 𝑣 → 𝜃 ) ) )
43 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ suc 𝑣 ↔ 𝑦 ≈ suc 𝑣 ) )
44 43 3 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ( 𝑦 ≈ suc 𝑣 → 𝜃 ) ) )
45 44 cbvalvw ⊢ ( ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ≈ suc 𝑣 → 𝜃 ) )
46 42 45 imbitrrdi ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
47 10 13 16 20 46 finds1 ⊢ ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) )
48 47 19.21bi ⊢ ( 𝑤 ∈ ω → ( 𝑥 ≈ 𝑤 → 𝜑 ) )
49 48 rexlimiv ⊢ ( ∃ 𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑 )
50 7 49 sylbi ⊢ ( 𝑥 ∈ Fin → 𝜑 )
51 4 50 vtoclga ⊢ ( 𝐴 ∈ Fin → 𝜏 )