![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brfi1uzind | Structured version Visualization version GIF version |
Description: Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with 𝐿 = 0 (see brfi1ind 13362) or 𝐿 = 1. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Proof shortened by AV, 23-Oct-2020.) (Revised by AV, 28-Mar-2021.) |
Ref | Expression |
---|---|
brfi1uzind.r | ⊢ Rel 𝐺 |
brfi1uzind.f | ⊢ 𝐹 ∈ V |
brfi1uzind.l | ⊢ 𝐿 ∈ ℕ0 |
brfi1uzind.1 | ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) |
brfi1uzind.2 | ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) |
brfi1uzind.3 | ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) |
brfi1uzind.4 | ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) |
brfi1uzind.base | ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝐿) → 𝜓) |
brfi1uzind.step | ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) |
Ref | Expression |
---|---|
brfi1uzind | ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brfi1uzind.r | . . . 4 ⊢ Rel 𝐺 | |
2 | brrelex12 5232 | . . . 4 ⊢ ((Rel 𝐺 ∧ 𝑉𝐺𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) | |
3 | 1, 2 | mpan 708 | . . 3 ⊢ (𝑉𝐺𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | simpl 474 | . . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝑉 ∈ V) | |
5 | simplr 809 | . . . . . 6 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑎 = 𝑉) → 𝐸 ∈ V) | |
6 | breq12 4733 | . . . . . . 7 ⊢ ((𝑎 = 𝑉 ∧ 𝑏 = 𝐸) → (𝑎𝐺𝑏 ↔ 𝑉𝐺𝐸)) | |
7 | 6 | adantll 752 | . . . . . 6 ⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑎 = 𝑉) ∧ 𝑏 = 𝐸) → (𝑎𝐺𝑏 ↔ 𝑉𝐺𝐸)) |
8 | 5, 7 | sbcied 3546 | . . . . 5 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑎 = 𝑉) → ([𝐸 / 𝑏]𝑎𝐺𝑏 ↔ 𝑉𝐺𝐸)) |
9 | 4, 8 | sbcied 3546 | . . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ([𝑉 / 𝑎][𝐸 / 𝑏]𝑎𝐺𝑏 ↔ 𝑉𝐺𝐸)) |
10 | 9 | biimprcd 240 | . . 3 ⊢ (𝑉𝐺𝐸 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → [𝑉 / 𝑎][𝐸 / 𝑏]𝑎𝐺𝑏)) |
11 | 3, 10 | mpd 15 | . 2 ⊢ (𝑉𝐺𝐸 → [𝑉 / 𝑎][𝐸 / 𝑏]𝑎𝐺𝑏) |
12 | brfi1uzind.f | . . 3 ⊢ 𝐹 ∈ V | |
13 | brfi1uzind.l | . . 3 ⊢ 𝐿 ∈ ℕ0 | |
14 | brfi1uzind.1 | . . 3 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) | |
15 | brfi1uzind.2 | . . 3 ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) | |
16 | vex 3275 | . . . . 5 ⊢ 𝑣 ∈ V | |
17 | vex 3275 | . . . . 5 ⊢ 𝑒 ∈ V | |
18 | breq12 4733 | . . . . 5 ⊢ ((𝑎 = 𝑣 ∧ 𝑏 = 𝑒) → (𝑎𝐺𝑏 ↔ 𝑣𝐺𝑒)) | |
19 | 16, 17, 18 | sbc2ie 3579 | . . . 4 ⊢ ([𝑣 / 𝑎][𝑒 / 𝑏]𝑎𝐺𝑏 ↔ 𝑣𝐺𝑒) |
20 | brfi1uzind.3 | . . . . 5 ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) | |
21 | difexg 4884 | . . . . . . 7 ⊢ (𝑣 ∈ V → (𝑣 ∖ {𝑛}) ∈ V) | |
22 | 16, 21 | ax-mp 5 | . . . . . 6 ⊢ (𝑣 ∖ {𝑛}) ∈ V |
23 | 12 | elexi 3285 | . . . . . 6 ⊢ 𝐹 ∈ V |
24 | breq12 4733 | . . . . . 6 ⊢ ((𝑎 = (𝑣 ∖ {𝑛}) ∧ 𝑏 = 𝐹) → (𝑎𝐺𝑏 ↔ (𝑣 ∖ {𝑛})𝐺𝐹)) | |
25 | 22, 23, 24 | sbc2ie 3579 | . . . . 5 ⊢ ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝑎𝐺𝑏 ↔ (𝑣 ∖ {𝑛})𝐺𝐹) |
26 | 20, 25 | sylibr 224 | . . . 4 ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝑎𝐺𝑏) |
27 | 19, 26 | sylanb 490 | . . 3 ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝑎𝐺𝑏 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝑎𝐺𝑏) |
28 | brfi1uzind.4 | . . 3 ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) | |
29 | brfi1uzind.base | . . . 4 ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝐿) → 𝜓) | |
30 | 19, 29 | sylanb 490 | . . 3 ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝑎𝐺𝑏 ∧ (♯‘𝑣) = 𝐿) → 𝜓) |
31 | 19 | 3anbi1i 1326 | . . . . 5 ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝑎𝐺𝑏 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) |
32 | 31 | anbi2i 732 | . . . 4 ⊢ (((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝑎𝐺𝑏 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ↔ ((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) |
33 | brfi1uzind.step | . . . 4 ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) | |
34 | 32, 33 | sylanb 490 | . . 3 ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝑎𝐺𝑏 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) |
35 | 12, 13, 14, 15, 27, 28, 30, 34 | fi1uzind 13360 | . 2 ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝑎𝐺𝑏 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) |
36 | 11, 35 | syl3an1 1440 | 1 ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 = wceq 1564 ∈ wcel 2071 Vcvv 3272 [wsbc 3509 ∖ cdif 3645 {csn 4253 class class class wbr 4728 Rel wrel 5191 ‘cfv 5969 (class class class)co 6733 Fincfn 8040 1c1 10018 + caddc 10020 ≤ cle 10156 ℕ0cn0 11373 ♯chash 13200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-8 2073 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-rep 4847 ax-sep 4857 ax-nul 4865 ax-pow 4916 ax-pr 4979 ax-un 7034 ax-cnex 10073 ax-resscn 10074 ax-1cn 10075 ax-icn 10076 ax-addcl 10077 ax-addrcl 10078 ax-mulcl 10079 ax-mulrcl 10080 ax-mulcom 10081 ax-addass 10082 ax-mulass 10083 ax-distr 10084 ax-i2m1 10085 ax-1ne0 10086 ax-1rid 10087 ax-rnegex 10088 ax-rrecex 10089 ax-cnre 10090 ax-pre-lttri 10091 ax-pre-lttrn 10092 ax-pre-ltadd 10093 ax-pre-mulgt0 10094 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-eu 2543 df-mo 2544 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ne 2865 df-nel 2968 df-ral 2987 df-rex 2988 df-reu 2989 df-rmo 2990 df-rab 2991 df-v 3274 df-sbc 3510 df-csb 3608 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-pss 3664 df-nul 3992 df-if 4163 df-pw 4236 df-sn 4254 df-pr 4256 df-tp 4258 df-op 4260 df-uni 4513 df-int 4552 df-iun 4598 df-br 4729 df-opab 4789 df-mpt 4806 df-tr 4829 df-id 5096 df-eprel 5101 df-po 5107 df-so 5108 df-fr 5145 df-we 5147 df-xp 5192 df-rel 5193 df-cnv 5194 df-co 5195 df-dm 5196 df-rn 5197 df-res 5198 df-ima 5199 df-pred 5761 df-ord 5807 df-on 5808 df-lim 5809 df-suc 5810 df-iota 5932 df-fun 5971 df-fn 5972 df-f 5973 df-f1 5974 df-fo 5975 df-f1o 5976 df-fv 5977 df-riota 6694 df-ov 6736 df-oprab 6737 df-mpt2 6738 df-om 7151 df-1st 7253 df-2nd 7254 df-wrecs 7495 df-recs 7556 df-rdg 7594 df-1o 7648 df-oadd 7652 df-er 7830 df-en 8041 df-dom 8042 df-sdom 8043 df-fin 8044 df-card 8846 df-cda 9071 df-pnf 10157 df-mnf 10158 df-xr 10159 df-ltxr 10160 df-le 10161 df-sub 10349 df-neg 10350 df-nn 11102 df-n0 11374 df-xnn0 11445 df-z 11459 df-uz 11769 df-fz 12409 df-hash 13201 |
This theorem is referenced by: brfi1ind 13362 |
Copyright terms: Public domain | W3C validator |