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

Theorem findcard2 6950
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 6820 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 4037 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 231 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1838 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 4037 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 231 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1838 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 4037 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 231 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1838 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 6854 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2.5 . . . . . . . . 9 𝜓
14 findcard2.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 168 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 121 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1463 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 peano3 4632 . . . . . . . . . . . . 13 (𝑣 ∈ ω → suc 𝑣 ≠ ∅)
1918adantr 276 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅)
20 breq1 4036 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2120anbi2d 464 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
22 peano1 4630 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
23 peano2 4631 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
24 nneneq 6918 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2522, 23, 24sylancr 414 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2625biimpa 296 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2726eqcomd 2202 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2821, 27biimtrdi 163 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2928com12 30 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
3029necon3d 2411 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3119, 30mpd 13 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3231ex 115 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
33 nnfi 6933 . . . . . . . . . . . . . . . 16 (suc 𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3423, 33syl 14 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3534adantr 276 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin)
36 enfi 6934 . . . . . . . . . . . . . . 15 (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3736adantl 277 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3835, 37mpbird 167 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin)
39 fin0 6946 . . . . . . . . . . . . 13 (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
4038, 39syl 14 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
41 simpll 527 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → 𝑣 ∈ ω)
42 dif1en 6940 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
43423expa 1205 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
44 fidifsnid 6932 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ Fin ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
4538, 44sylan 283 . . . . . . . . . . . . . . . 16 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
46 vex 2766 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
47 difexg 4174 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑤 ∖ {𝑧}) ∈ V
49 breq1 4036 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
5049anbi2d 464 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
51 uneq1 3310 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
5251sbceq1d 2994 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
5352imbi2d 230 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
5450, 53imbi12d 234 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
55 breq1 4036 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
56 findcard2.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝜑𝜒))
5755, 56imbi12d 234 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
5857spv 1874 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
59 rspe 2546 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
60 isfi 6820 . . . . . . . . . . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
68 vex 2766 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
6968snex 4218 . . . . . . . . . . . . . . . . . . . . 21 {𝑧} ∈ V
7067, 69unex 4476 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∪ {𝑧}) ∈ V
71 findcard2.3 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
7270, 71sbcie 3024 . . . . . . . . . . . . . . . . . . 19 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
7366, 72imbitrrdi 162 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
7448, 54, 73vtocl 2818 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
75 dfsbcq 2991 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
7675imbi2d 230 . . . . . . . . . . . . . . . . 17 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7774, 76imbitrid 154 . . . . . . . . . . . . . . . 16 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7845, 77syl 14 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7941, 43, 78mp2and 433 . . . . . . . . . . . . . 14 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))
8079ex 115 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8180exlimdv 1833 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8240, 81sylbid 150 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8382ex 115 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
8432, 83mpdd 41 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8584com23 78 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
8685alrimdv 1890 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
87 nfv 1542 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
88 nfv 1542 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
89 nfsbc1v 3008 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
9088, 89nfim 1586 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
91 breq1 4036 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
92 sbceq1a 2999 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
9391, 92imbi12d 234 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
9487, 90, 93cbval 1768 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
9586, 94imbitrrdi 162 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
965, 8, 11, 17, 95finds1 4638 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
979619.21bi 1572 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
9897rexlimiv 2608 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
992, 98sylbi 121 . 2 (𝑥 ∈ Fin → 𝜑)
1001, 99vtoclga 2830 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1362   = wceq 1364  wex 1506  wcel 2167  wne 2367  wrex 2476  Vcvv 2763  [wsbc 2989  cdif 3154  cun 3155  c0 3450  {csn 3622   class class class wbr 4033  suc csuc 4400  ωcom 4626  cen 6797  Fincfn 6799
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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-iord 4401  df-on 4403  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-er 6592  df-en 6800  df-fin 6802
This theorem is referenced by:  finomni  7206  rexfiuz  11154  fimaxre2  11392
  Copyright terms: Public domain W3C validator