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