Metamath Proof Explorer

Theorem findcard2

Description: Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 findcard2.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2 findcard2.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 findcard2.3 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝜑 ↔ 𝜃 ) )
4 findcard2.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 findcard2.5 ⊢ 𝜓
6 findcard2.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 rexdif1en ⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ∃ 𝑧 ∈ 𝑤 ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 )
22 snssi ⊢ ( 𝑧 ∈ 𝑤 → { 𝑧 } ⊆ 𝑤 )
23 uncom ⊢ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = ( { 𝑧 } ∪ ( 𝑤 ∖ { 𝑧 } ) )
24 undif ⊢ ( { 𝑧 } ⊆ 𝑤 ↔ ( { 𝑧 } ∪ ( 𝑤 ∖ { 𝑧 } ) ) = 𝑤 )
25 24 biimpi ⊢ ( { 𝑧 } ⊆ 𝑤 → ( { 𝑧 } ∪ ( 𝑤 ∖ { 𝑧 } ) ) = 𝑤 )
26 23 25 eqtrid ⊢ ( { 𝑧 } ⊆ 𝑤 → ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 )
27 vex ⊢ 𝑤 ∈ V
28 27 difexi ⊢ ( 𝑤 ∖ { 𝑧 } ) ∈ V
29 breq1 ⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( 𝑦 ≈ 𝑣 ↔ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) )
30 29 anbi2d ⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) ↔ ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) ) )
31 uneq1 ⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( 𝑦 ∪ { 𝑧 } ) = ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
32 31 sbceq1d ⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) )
33 32 imbi2d ⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ) )
34 30 33 imbi12d ⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ) ) )
35 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣 ) )
36 35 2 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ 𝑣 → 𝜑 ) ↔ ( 𝑦 ≈ 𝑣 → 𝜒 ) ) )
37 36 spvv ⊢ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( 𝑦 ≈ 𝑣 → 𝜒 ) )
38 rspe ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ∃ 𝑣 ∈ ω 𝑦 ≈ 𝑣 )
39 isfi ⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑣 ∈ ω 𝑦 ≈ 𝑣 )
40 38 39 sylibr ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → 𝑦 ∈ Fin )
41 pm2.27 ⊢ ( 𝑦 ≈ 𝑣 → ( ( 𝑦 ≈ 𝑣 → 𝜒 ) → 𝜒 ) )
42 41 adantl ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ( 𝑦 ≈ 𝑣 → 𝜒 ) → 𝜒 ) )
43 40 42 6 sylsyld ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ( 𝑦 ≈ 𝑣 → 𝜒 ) → 𝜃 ) )
44 37 43 syl5 ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → 𝜃 ) )
45 vex ⊢ 𝑦 ∈ V
46 snex ⊢ { 𝑧 } ∈ V
47 45 46 unex ⊢ ( 𝑦 ∪ { 𝑧 } ) ∈ V
48 47 3 sbcie ⊢ ( [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ↔ 𝜃 )
49 44 48 syl6ibr ⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) )
50 28 34 49 vtocl ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) )
51 dfsbcq ⊢ ( ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 → ( [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
52 51 imbi2d ⊢ ( ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 → ( ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
53 50 52 syl5ib ⊢ ( ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 → ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
54 22 26 53 3syl ⊢ ( 𝑧 ∈ 𝑤 → ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
55 54 expd ⊢ ( 𝑧 ∈ 𝑤 → ( 𝑣 ∈ ω → ( ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
56 55 com12 ⊢ ( 𝑣 ∈ ω → ( 𝑧 ∈ 𝑤 → ( ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
57 56 rexlimdv ⊢ ( 𝑣 ∈ ω → ( ∃ 𝑧 ∈ 𝑤 ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
58 57 adantr ⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( ∃ 𝑧 ∈ 𝑤 ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
59 21 58 mpd ⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) )
60 59 ex ⊢ ( 𝑣 ∈ ω → ( 𝑤 ≈ suc 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
61 60 com23 ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
62 61 alrimdv ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑤 ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
63 nfv ⊢ Ⅎ 𝑤 ( 𝑥 ≈ suc 𝑣 → 𝜑 )
64 nfv ⊢ Ⅎ 𝑥 𝑤 ≈ suc 𝑣
65 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
66 64 65 nfim ⊢ Ⅎ 𝑥 ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 )
67 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣 ) )
68 sbceq1a ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
69 67 68 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
70 63 66 69 cbvalv1 ⊢ ( ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ∀ 𝑤 ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) )
71 62 70 syl6ibr ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
72 10 13 16 20 71 finds1 ⊢ ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) )
73 72 19.21bi ⊢ ( 𝑤 ∈ ω → ( 𝑥 ≈ 𝑤 → 𝜑 ) )
74 73 rexlimiv ⊢ ( ∃ 𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑 )
75 7 74 sylbi ⊢ ( 𝑥 ∈ Fin → 𝜑 )
76 4 75 vtoclga ⊢ ( 𝐴 ∈ Fin → 𝜏 )