Metamath Proof Explorer

Theorem findcard4

Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any set with less elements. The result is then proven to be true for all finite sets. (Contributed by Thomas van Maaren, 14-Aug-2026)

Ref Expression
Hypotheses findcard4.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
findcard4.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
findcard4.3 ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → 𝜑 ) → 𝜒 ) )
Assertion findcard4 ( 𝐴 ∈ Fin → 𝜏 )

Proof

Step Hyp Ref Expression
1 findcard4.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
2 findcard4.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
3 findcard4.3 ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → 𝜑 ) → 𝜒 ) )
4 ficardom ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
5 nnfi ⊢ ( ( card ‘ 𝐴 ) ∈ ω → ( card ‘ 𝐴 ) ∈ Fin )
6 4 5 syl ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ Fin )
7 fveq2 ⊢ ( 𝑥 = 𝑦 → ( card ‘ 𝑥 ) = ( card ‘ 𝑦 ) )
8 7 adantl ⊢ ( ( 𝑤 = 𝑧 ∧ 𝑥 = 𝑦 ) → ( card ‘ 𝑥 ) = ( card ‘ 𝑦 ) )
9 simpl ⊢ ( ( 𝑤 = 𝑧 ∧ 𝑥 = 𝑦 ) → 𝑤 = 𝑧 )
10 8 9 eqeq12d ⊢ ( ( 𝑤 = 𝑧 ∧ 𝑥 = 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 ↔ ( card ‘ 𝑦 ) = 𝑧 ) )
11 1 adantl ⊢ ( ( 𝑤 = 𝑧 ∧ 𝑥 = 𝑦 ) → ( 𝜑 ↔ 𝜒 ) )
12 10 11 imbi12d ⊢ ( ( 𝑤 = 𝑧 ∧ 𝑥 = 𝑦 ) → ( ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ↔ ( ( card ‘ 𝑦 ) = 𝑧 → 𝜒 ) ) )
13 12 cbvaldvaw ⊢ ( 𝑤 = 𝑧 → ( ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ↔ ∀ 𝑦 ( ( card ‘ 𝑦 ) = 𝑧 → 𝜒 ) ) )
14 eqeq2 ⊢ ( 𝑤 = ( card ‘ 𝐴 ) → ( ( card ‘ 𝑥 ) = 𝑤 ↔ ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) )
15 14 imbi1d ⊢ ( 𝑤 = ( card ‘ 𝐴 ) → ( ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ↔ ( ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) → 𝜑 ) ) )
16 15 albidv ⊢ ( 𝑤 = ( card ‘ 𝐴 ) → ( ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) → 𝜑 ) ) )
17 eleq1 ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ( card ‘ 𝑦 ) ∈ Fin ↔ 𝑧 ∈ Fin ) )
18 vex ⊢ 𝑦 ∈ V
19 18 cardid ⊢ ( card ‘ 𝑦 ) ≈ 𝑦
20 enfi ⊢ ( ( card ‘ 𝑦 ) ≈ 𝑦 → ( ( card ‘ 𝑦 ) ∈ Fin ↔ 𝑦 ∈ Fin ) )
21 19 20 ax-mp ⊢ ( ( card ‘ 𝑦 ) ∈ Fin ↔ 𝑦 ∈ Fin )
22 17 21 bitr3di ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( 𝑧 ∈ Fin ↔ 𝑦 ∈ Fin ) )
23 22 biimpd ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( 𝑧 ∈ Fin → 𝑦 ∈ Fin ) )
24 psseq2 ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( 𝑤 ⊊ ( card ‘ 𝑦 ) ↔ 𝑤 ⊊ 𝑧 ) )
25 24 bicomd ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( 𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ ( card ‘ 𝑦 ) ) )
26 25 imbi1d ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) ↔ ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) ) )
27 sp ⊢ ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝑤 ⊊ ( card ‘ 𝑦 ) )
28 27 imim1i ⊢ ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) )
29 axi5r ⊢ ( ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑥 ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) )
30 ax-5 ⊢ ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) )
31 30 imim1i ⊢ ( ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) )
32 eqcom ⊢ ( 𝑤 = ( card ‘ 𝑥 ) ↔ ( card ‘ 𝑥 ) = 𝑤 )
33 pm2.04 ⊢ ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ( ( card ‘ 𝑥 ) = 𝑤 → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
34 32 33 biimtrid ⊢ ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
35 31 34 syl ⊢ ( ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
36 35 alimi ⊢ ( ∀ 𝑥 ( ∀ 𝑥 𝑤 ⊊ ( card ‘ 𝑦 ) → ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑥 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
37 28 29 36 3syl ⊢ ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑥 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
38 26 37 biimtrdi ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑥 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) )
39 38 alimdv ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ∀ 𝑤 ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑤 ∀ 𝑥 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) )
40 ax-11 ⊢ ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → ∀ 𝑥 ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
41 40 a1i ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → ∀ 𝑥 ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) )
42 nfvd ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → Ⅎ 𝑤 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) )
43 psseq1 ⊢ ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) ↔ ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) ) )
44 43 imbi1d ⊢ ( 𝑤 = ( card ‘ 𝑥 ) → ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ↔ ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
45 44 a1i ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( 𝑤 = ( card ‘ 𝑥 ) → ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ↔ ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) )
46 45 alrimiv ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ↔ ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) )
47 fvexd ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( card ‘ 𝑥 ) ∈ V )
48 ceqsalt ⊢ ( ( Ⅎ 𝑤 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ∧ ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ↔ ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) ∧ ( card ‘ 𝑥 ) ∈ V ) → ( ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ↔ ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
49 48 biimpd ⊢ ( ( Ⅎ 𝑤 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ∧ ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ↔ ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) ) ∧ ( card ‘ 𝑥 ) ∈ V ) → ( ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
50 42 46 47 49 syl3anc ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
51 50 alimdv ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 = ( card ‘ 𝑥 ) → ( 𝑤 ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
52 39 41 51 3syld ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ∀ 𝑤 ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑥 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) )
53 hashxnn0 ⊢ ( 𝑥 ∈ V → ( ♯ ‘ 𝑥 ) ∈ ℕ0* )
54 53 elv ⊢ ( ♯ ‘ 𝑥 ) ∈ ℕ0*
55 hashcl ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
56 hashxrcl ⊢ ( 𝑥 ∈ V → ( ♯ ‘ 𝑥 ) ∈ ℝ* )
57 56 elv ⊢ ( ♯ ‘ 𝑥 ) ∈ ℝ*
58 hashxrcl ⊢ ( 𝑦 ∈ V → ( ♯ ‘ 𝑦 ) ∈ ℝ* )
59 58 elv ⊢ ( ♯ ‘ 𝑦 ) ∈ ℝ*
60 xrltle ⊢ ( ( ( ♯ ‘ 𝑥 ) ∈ ℝ* ∧ ( ♯ ‘ 𝑦 ) ∈ ℝ* ) → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑦 ) ) )
61 57 59 60 mp2an ⊢ ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑦 ) )
62 xnn0lenn0nn0 ⊢ ( ( ( ♯ ‘ 𝑥 ) ∈ ℕ0* ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑦 ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
63 54 55 61 62 mp3an3an ⊢ ( ( 𝑦 ∈ Fin ∧ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
64 hashclb ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ Fin ↔ ( ♯ ‘ 𝑥 ) ∈ ℕ0 ) )
65 64 elv ⊢ ( 𝑥 ∈ Fin ↔ ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
66 63 65 sylibr ⊢ ( ( 𝑦 ∈ Fin ∧ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) → 𝑥 ∈ Fin )
67 hashsdom ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ↔ 𝑥 ≺ 𝑦 ) )
68 cardsdom ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ↔ 𝑥 ≺ 𝑦 ) )
69 68 el2v ⊢ ( ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ↔ 𝑥 ≺ 𝑦 )
70 67 69 bitr4di ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ↔ ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ) )
71 70 biimpd ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ) )
72 71 expimpd ⊢ ( 𝑥 ∈ Fin → ( ( 𝑦 ∈ Fin ∧ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) → ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ) )
73 66 72 mpcom ⊢ ( ( 𝑦 ∈ Fin ∧ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) → ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) )
74 73 ex ⊢ ( 𝑦 ∈ Fin → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ) )
75 cardon ⊢ ( card ‘ 𝑥 ) ∈ On
76 75 onordi ⊢ Ord ( card ‘ 𝑥 )
77 cardon ⊢ ( card ‘ 𝑦 ) ∈ On
78 77 onordi ⊢ Ord ( card ‘ 𝑦 )
79 ordelpss ⊢ ( ( Ord ( card ‘ 𝑥 ) ∧ Ord ( card ‘ 𝑦 ) ) → ( ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ↔ ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) ) )
80 76 78 79 mp2an ⊢ ( ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ↔ ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) )
81 74 80 imbitrdi ⊢ ( 𝑦 ∈ Fin → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) ) )
82 81 imim1d ⊢ ( 𝑦 ∈ Fin → ( ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) → ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → 𝜑 ) ) )
83 82 alimdv ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) → ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) → 𝜑 ) ) )
84 83 3 syld ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) → 𝜒 ) )
85 84 imp ⊢ ( ( 𝑦 ∈ Fin ∧ ∀ 𝑥 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → 𝜒 )
86 85 a1i ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ( 𝑦 ∈ Fin ∧ ∀ 𝑥 ( ( card ‘ 𝑥 ) ⊊ ( card ‘ 𝑦 ) → 𝜑 ) ) → 𝜒 ) )
87 23 52 86 syl2and ⊢ ( ( card ‘ 𝑦 ) = 𝑧 → ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) ) → 𝜒 ) )
88 87 com12 ⊢ ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) ) → ( ( card ‘ 𝑦 ) = 𝑧 → 𝜒 ) )
89 88 alrimiv ⊢ ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) ) → ∀ 𝑦 ( ( card ‘ 𝑦 ) = 𝑧 → 𝜒 ) )
90 89 ex ⊢ ( 𝑧 ∈ Fin → ( ∀ 𝑤 ( 𝑤 ⊊ 𝑧 → ∀ 𝑥 ( ( card ‘ 𝑥 ) = 𝑤 → 𝜑 ) ) → ∀ 𝑦 ( ( card ‘ 𝑦 ) = 𝑧 → 𝜒 ) ) )
91 13 16 90 findcard3 ⊢ ( ( card ‘ 𝐴 ) ∈ Fin → ∀ 𝑥 ( ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) → 𝜑 ) )
92 fveq2 ⊢ ( 𝑥 = 𝐴 → ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
93 92 imim1i ⊢ ( ( ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) → 𝜑 ) → ( 𝑥 = 𝐴 → 𝜑 ) )
94 93 alimi ⊢ ( ∀ 𝑥 ( ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) )
95 6 91 94 3syl ⊢ ( 𝐴 ∈ Fin → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) )
96 nfvd ⊢ ( 𝐴 ∈ Fin → Ⅎ 𝑥 𝜏 )
97 2 ax-gen ⊢ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
98 97 a1i ⊢ ( 𝐴 ∈ Fin → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) ) )
99 id ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ Fin )
100 ceqsalt ⊢ ( ( Ⅎ 𝑥 𝜏 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) ) ∧ 𝐴 ∈ Fin ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜏 ) )
101 96 98 99 100 syl3anc ⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜏 ) )
102 95 101 mpbid ⊢ ( 𝐴 ∈ Fin → 𝜏 )