ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  findcard2 GIF version

Theorem findcard2 6891
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.)
Hypotheses
Ref Expression
findcard2.1 (𝑥 = ∅ → (𝜑𝜓))
findcard2.2 (𝑥 = 𝑦 → (𝜑𝜒))
findcard2.3 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
findcard2.4 (𝑥 = 𝐴 → (𝜑𝜏))
findcard2.5 𝜓
findcard2.6 (𝑦 ∈ Fin → (𝜒𝜃))
Assertion
Ref Expression
findcard2 (𝐴 ∈ Fin → 𝜏)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard2
Dummy variables 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2.4 . 2 (𝑥 = 𝐴 → (𝜑𝜏))
2 isfi 6763 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 4009 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 231 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1824 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 4009 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 231 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1824 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 4009 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 231 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1824 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 6797 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2.5 . . . . . . . . 9 𝜓
14 findcard2.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 168 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 121 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1449 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 peano3 4597 . . . . . . . . . . . . 13 (𝑣 ∈ ω → suc 𝑣 ≠ ∅)
1918adantr 276 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅)
20 breq1 4008 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2120anbi2d 464 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
22 peano1 4595 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
23 peano2 4596 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
24 nneneq 6859 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2522, 23, 24sylancr 414 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2625biimpa 296 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2726eqcomd 2183 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2821, 27biimtrdi 163 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2928com12 30 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
3029necon3d 2391 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3119, 30mpd 13 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3231ex 115 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
33 nnfi 6874 . . . . . . . . . . . . . . . 16 (suc 𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3423, 33syl 14 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3534adantr 276 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin)
36 enfi 6875 . . . . . . . . . . . . . . 15 (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3736adantl 277 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3835, 37mpbird 167 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin)
39 fin0 6887 . . . . . . . . . . . . 13 (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
4038, 39syl 14 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
41 simpll 527 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → 𝑣 ∈ ω)
42 dif1en 6881 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
43423expa 1203 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
44 fidifsnid 6873 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ Fin ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
4538, 44sylan 283 . . . . . . . . . . . . . . . 16 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
46 vex 2742 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
47 difexg 4146 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑤 ∖ {𝑧}) ∈ V
49 breq1 4008 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
5049anbi2d 464 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
51 uneq1 3284 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
5251sbceq1d 2969 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
5352imbi2d 230 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
5450, 53imbi12d 234 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
55 breq1 4008 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
56 findcard2.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝜑𝜒))
5755, 56imbi12d 234 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
5857spv 1860 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
59 rspe 2526 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
60 isfi 6763 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦𝑣)
6159, 60sylibr 134 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ∈ ω ∧ 𝑦𝑣) → 𝑦 ∈ Fin)
62 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑣 → ((𝑦𝑣𝜒) → 𝜒))
6362adantl 277 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜒))
64 findcard2.6 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ Fin → (𝜒𝜃))
6561, 63, 64sylsyld 58 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜃))
6658, 65syl5 32 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → 𝜃))
67 vex 2742 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
68 vex 2742 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
6968snex 4187 . . . . . . . . . . . . . . . . . . . . 21 {𝑧} ∈ V
7067, 69unex 4443 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∪ {𝑧}) ∈ V
71 findcard2.3 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
7270, 71sbcie 2999 . . . . . . . . . . . . . . . . . . 19 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
7366, 72imbitrrdi 162 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
7448, 54, 73vtocl 2793 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
75 dfsbcq 2966 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
7675imbi2d 230 . . . . . . . . . . . . . . . . 17 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7774, 76imbitrid 154 . . . . . . . . . . . . . . . 16 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7845, 77syl 14 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7941, 43, 78mp2and 433 . . . . . . . . . . . . . 14 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))
8079ex 115 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8180exlimdv 1819 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8240, 81sylbid 150 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8382ex 115 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
8432, 83mpdd 41 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8584com23 78 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
8685alrimdv 1876 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
87 nfv 1528 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
88 nfv 1528 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
89 nfsbc1v 2983 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
9088, 89nfim 1572 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
91 breq1 4008 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
92 sbceq1a 2974 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
9391, 92imbi12d 234 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
9487, 90, 93cbval 1754 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
9586, 94imbitrrdi 162 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
965, 8, 11, 17, 95finds1 4603 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
979619.21bi 1558 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
9897rexlimiv 2588 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
992, 98sylbi 121 . 2 (𝑥 ∈ Fin → 𝜑)
1001, 99vtoclga 2805 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1351   = wceq 1353  wex 1492  wcel 2148  wne 2347  wrex 2456  Vcvv 2739  [wsbc 2964  cdif 3128  cun 3129  c0 3424  {csn 3594   class class class wbr 4005  suc csuc 4367  ωcom 4591  cen 6740  Fincfn 6742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-er 6537  df-en 6743  df-fin 6745
This theorem is referenced by:  finomni  7140  rexfiuz  11000  fimaxre2  11237
  Copyright terms: Public domain W3C validator