MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  findcard2 Structured version   Visualization version   GIF version

Theorem findcard2 8160
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 7939 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 4627 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 331 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1846 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 4627 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 331 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1846 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 4627 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 331 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1846 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 7979 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2.5 . . . . . . . . 9 𝜓
14 findcard2.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 248 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 207 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1719 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 nsuceq0 5774 . . . . . . . . . . . 12 suc 𝑣 ≠ ∅
19 breq1 4626 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2019anbi2d 739 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
21 peano1 7047 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
22 peano2 7048 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
23 nneneq 8103 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2421, 22, 23sylancr 694 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2524biimpa 501 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2625eqcomd 2627 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2720, 26syl6bi 243 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2827com12 32 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
2928necon3d 2811 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3018, 29mpi 20 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3130ex 450 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
32 n0 3913 . . . . . . . . . . . 12 (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤)
33 dif1en 8153 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
34333expia 1264 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (𝑤 ∖ {𝑧}) ≈ 𝑣))
35 snssi 4315 . . . . . . . . . . . . . . . . . 18 (𝑧𝑤 → {𝑧} ⊆ 𝑤)
36 uncom 3741 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝑤 ∖ {𝑧}))
37 undif 4027 . . . . . . . . . . . . . . . . . . . 20 ({𝑧} ⊆ 𝑤 ↔ ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
3837biimpi 206 . . . . . . . . . . . . . . . . . . 19 ({𝑧} ⊆ 𝑤 → ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
3936, 38syl5eq 2667 . . . . . . . . . . . . . . . . . 18 ({𝑧} ⊆ 𝑤 → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
40 vex 3193 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
41 difexg 4778 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
4240, 41ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∖ {𝑧}) ∈ V
43 breq1 4626 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
4443anbi2d 739 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
45 uneq1 3744 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
4645sbceq1d 3427 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
4746imbi2d 330 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
4844, 47imbi12d 334 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
49 breq1 4626 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
50 findcard2.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝜑𝜒))
5149, 50imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
5251spv 2259 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
53 rspe 2999 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
54 isfi 7939 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦𝑣)
5553, 54sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → 𝑦 ∈ Fin)
56 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑣 → ((𝑦𝑣𝜒) → 𝜒))
5756adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜒))
58 findcard2.6 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ Fin → (𝜒𝜃))
5955, 57, 58sylsyld 61 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜃))
6052, 59syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → 𝜃))
61 vex 3193 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦 ∈ V
62 snex 4879 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑧} ∈ V
6361, 62unex 6921 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∪ {𝑧}) ∈ V
64 findcard2.3 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
6563, 64sbcie 3457 . . . . . . . . . . . . . . . . . . . . 21 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
6660, 65syl6ibr 242 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
6742, 48, 66vtocl 3249 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
68 dfsbcq 3424 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
6968imbi2d 330 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7067, 69syl5ib 234 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7135, 39, 703syl 18 . . . . . . . . . . . . . . . . 17 (𝑧𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7271expd 452 . . . . . . . . . . . . . . . 16 (𝑧𝑤 → (𝑣 ∈ ω → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7372com12 32 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → (𝑧𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7473adantr 481 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7534, 74mpdd 43 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7675exlimdv 1858 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7732, 76syl5bi 232 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7877ex 450 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7931, 78mpdd 43 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8079com23 86 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
8180alrimdv 1854 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
82 nfv 1840 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
83 nfv 1840 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
84 nfsbc1v 3442 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
8583, 84nfim 1822 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
86 breq1 4626 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
87 sbceq1a 3433 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
8886, 87imbi12d 334 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
8982, 85, 88cbval 2270 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
9081, 89syl6ibr 242 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
915, 8, 11, 17, 90finds1 7057 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
929119.21bi 2057 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
9392rexlimiv 3022 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
942, 93sylbi 207 . 2 (𝑥 ∈ Fin → 𝜑)
951, 94vtoclga 3262 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wrex 2909  Vcvv 3190  [wsbc 3422  cdif 3557  cun 3558  wss 3560  c0 3897  {csn 4155   class class class wbr 4623  suc csuc 5694  ωcom 7027  cen 7912  Fincfn 7915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-om 7028  df-1o 7520  df-er 7702  df-en 7916  df-fin 7919
This theorem is referenced by:  findcard2s  8161  frfi  8165  fnfi  8198  iunfi  8214  finsschain  8233  infdiffi  8515  fin1a2lem10  9191  wunfi  9503  rexfiuz  14037  modfsummod  14472  lcmfunsnlem  15297  lcmfun  15301  drsdirfi  16878  fiuncmp  21147  finiunmbl  23252  mbfresfi  33127  heibor1lem  33279  pclfinclN  34755
  Copyright terms: Public domain W3C validator