| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hashcl 14396 | . . 3
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) | 
| 2 |  | dfclel 2816 | . . . 4
⊢
((♯‘𝑉)
∈ ℕ0 ↔ ∃𝑛(𝑛 = (♯‘𝑉) ∧ 𝑛 ∈
ℕ0)) | 
| 3 |  | eqeq2 2748 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 0 →
((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = 0)) | 
| 4 | 3 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑥 = 0 → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0))) | 
| 5 | 4 | imbi1d 341 | . . . . . . . . . . . 12
⊢ (𝑥 = 0 → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓))) | 
| 6 | 5 | 2albidv 1922 | . . . . . . . . . . 11
⊢ (𝑥 = 0 → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓))) | 
| 7 |  | eqeq2 2748 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = 𝑦)) | 
| 8 | 7 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦))) | 
| 9 | 8 | imbi1d 341 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓))) | 
| 10 | 9 | 2albidv 1922 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓))) | 
| 11 |  | eqeq2 2748 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 + 1) → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = (𝑦 + 1))) | 
| 12 | 11 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 + 1) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)))) | 
| 13 | 12 | imbi1d 341 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 + 1) → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓))) | 
| 14 | 13 | 2albidv 1922 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 + 1) → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓))) | 
| 15 |  | eqeq2 2748 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑛 → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = 𝑛)) | 
| 16 | 15 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛))) | 
| 17 | 16 | imbi1d 341 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑛 → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓))) | 
| 18 | 17 | 2albidv 1922 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓))) | 
| 19 |  | brfi1ind.base | . . . . . . . . . . . 12
⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓) | 
| 20 | 19 | gen2 1795 | . . . . . . . . . . 11
⊢
∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓) | 
| 21 |  | breq12 5147 | . . . . . . . . . . . . . . 15
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑣𝐺𝑒 ↔ 𝑤𝐺𝑓)) | 
| 22 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → ((♯‘𝑣) = 𝑦 ↔ (♯‘𝑤) = 𝑦)) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ((♯‘𝑣) = 𝑦 ↔ (♯‘𝑤) = 𝑦)) | 
| 24 | 21, 23 | anbi12d 632 | . . . . . . . . . . . . . 14
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) ↔ (𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦))) | 
| 25 |  | brfi1ind.2 | . . . . . . . . . . . . . 14
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) | 
| 26 | 24, 25 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓) ↔ ((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃))) | 
| 27 | 26 | cbval2vw 2038 | . . . . . . . . . . . 12
⊢
(∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓) ↔ ∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃)) | 
| 28 |  | nn0p1gt0 12557 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℕ0
→ 0 < (𝑦 +
1)) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝑣) =
(𝑦 + 1)) → 0 <
(𝑦 + 1)) | 
| 30 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝑣) =
(𝑦 + 1)) →
(♯‘𝑣) = (𝑦 + 1)) | 
| 31 | 29, 30 | breqtrrd 5170 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝑣) =
(𝑦 + 1)) → 0 <
(♯‘𝑣)) | 
| 32 | 31 | adantrl 716 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0
∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))) → 0 < (♯‘𝑣)) | 
| 33 |  | hashgt0elex 14441 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑣 ∈ V ∧ 0 <
(♯‘𝑣)) →
∃𝑛 𝑛 ∈ 𝑣) | 
| 34 |  | brfi1ind.3 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) | 
| 35 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝑣 ∈ V | 
| 36 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → 𝑛 ∈ 𝑣) | 
| 37 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → 𝑦 ∈ ℕ0) | 
| 38 |  | hashdifsnp1 14546 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑣 ∈ V ∧ 𝑛 ∈ 𝑣 ∧ 𝑦 ∈ ℕ0) →
((♯‘𝑣) = (𝑦 + 1) →
(♯‘(𝑣 ∖
{𝑛})) = 𝑦)) | 
| 39 | 35, 36, 37, 38 | mp3an2i 1467 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → ((♯‘𝑣) = (𝑦 + 1) → (♯‘(𝑣 ∖ {𝑛})) = 𝑦)) | 
| 40 | 39 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (♯‘(𝑣 ∖ {𝑛})) = 𝑦) | 
| 41 |  | peano2nn0 12568 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ0) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑦 + 1) ∈
ℕ0) | 
| 43 | 42 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → (𝑦 + 1) ∈
ℕ0) | 
| 44 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → 𝑣𝐺𝑒) | 
| 45 |  | simplrr 777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → (♯‘𝑣) = (𝑦 + 1)) | 
| 46 |  | simprlr 779 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) → 𝑛 ∈ 𝑣) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → 𝑛 ∈ 𝑣) | 
| 48 | 44, 45, 47 | 3jca 1128 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) | 
| 49 | 43, 48 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → ((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) | 
| 50 | 35 | difexi 5329 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑣 ∖ {𝑛}) ∈ V | 
| 51 |  | brfi1ind.f | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 𝐹 ∈ V | 
| 52 |  | breq12 5147 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝑤𝐺𝑓 ↔ (𝑣 ∖ {𝑛})𝐺𝐹)) | 
| 53 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑤 = (𝑣 ∖ {𝑛}) → ((♯‘𝑤) = 𝑦 ↔ (♯‘(𝑣 ∖ {𝑛})) = 𝑦)) | 
| 54 | 53 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ((♯‘𝑤) = 𝑦 ↔ (♯‘(𝑣 ∖ {𝑛})) = 𝑦)) | 
| 55 | 52, 54 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) ↔ ((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦))) | 
| 56 |  | brfi1ind.4 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) | 
| 57 | 55, 56 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ↔ (((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒))) | 
| 58 | 57 | spc2gv 3599 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑣 ∖ {𝑛}) ∈ V ∧ 𝐹 ∈ V) → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → (((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒))) | 
| 59 | 50, 51, 58 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → (((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒)) | 
| 60 | 59 | expdimp 452 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜒)) | 
| 61 | 60 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜒)) | 
| 62 |  | brfi1ind.step | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑦 + 1) ∈ ℕ0
∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) | 
| 63 | 49, 61, 62 | syl6an 684 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜓)) | 
| 64 | 63 | exp41 434 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑣𝐺𝑒 → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜓))))) | 
| 65 | 64 | com15 101 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘(𝑣
∖ {𝑛})) = 𝑦 → ((𝑣 ∖ {𝑛})𝐺𝐹 → (((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 66 | 65 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘(𝑣
∖ {𝑛})) = 𝑦 → (((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 67 | 40, 66 | mpcom 38 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))) | 
| 68 | 67 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → ((♯‘𝑣) = (𝑦 + 1) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 69 | 68 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 70 | 69 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℕ0
→ (𝑛 ∈ 𝑣 → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))) | 
| 71 | 70 | com15 101 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑣𝐺𝑒 → (𝑛 ∈ 𝑣 → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))) | 
| 72 | 71 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 73 | 34, 72 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))) | 
| 74 | 73 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣𝐺𝑒 → (𝑛 ∈ 𝑣 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 75 | 74 | com4l 92 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝑣 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 76 | 75 | exlimiv 1929 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑛 𝑛 ∈ 𝑣 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 77 | 33, 76 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑣 ∈ V ∧ 0 <
(♯‘𝑣)) →
((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 78 | 77 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ V → (0 <
(♯‘𝑣) →
((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))) | 
| 79 | 78 | com25 99 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ V → (𝑣𝐺𝑒 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (0 <
(♯‘𝑣) →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))) | 
| 80 | 79 | elv 3484 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣𝐺𝑒 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (0 <
(♯‘𝑣) →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))) | 
| 81 | 80 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑦 ∈ ℕ0 → (0 <
(♯‘𝑣) →
(∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))) | 
| 82 | 81 | impcom 407 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0
∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))) → (0 < (♯‘𝑣) → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))) | 
| 83 | 32, 82 | mpd 15 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0
∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))) → (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)) | 
| 84 | 83 | impancom 451 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0
∧ ∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃)) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓)) | 
| 85 | 84 | alrimivv 1927 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃)) → ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓)) | 
| 86 | 85 | ex 412 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ (∀𝑤∀𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓))) | 
| 87 | 27, 86 | biimtrid 242 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓) → ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓))) | 
| 88 | 6, 10, 14, 18, 20, 87 | nn0ind 12715 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓)) | 
| 89 |  | brfi1ind.r | . . . . . . . . . . . . 13
⊢ Rel 𝐺 | 
| 90 | 89 | brrelex12i 5739 | . . . . . . . . . . . 12
⊢ (𝑉𝐺𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) | 
| 91 |  | breq12 5147 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣𝐺𝑒 ↔ 𝑉𝐺𝐸)) | 
| 92 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑉 → ((♯‘𝑣) = 𝑛 ↔ (♯‘𝑉) = 𝑛)) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((♯‘𝑣) = 𝑛 ↔ (♯‘𝑉) = 𝑛)) | 
| 94 | 91, 93 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) ↔ (𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛))) | 
| 95 |  | brfi1ind.1 | . . . . . . . . . . . . . . . 16
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) | 
| 96 | 94, 95 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) ↔ ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → 𝜑))) | 
| 97 | 96 | spc2gv 3599 | . . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → 𝜑))) | 
| 98 | 97 | com23 86 | . . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑))) | 
| 99 | 98 | expd 415 | . . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉𝐺𝐸 → ((♯‘𝑉) = 𝑛 → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑)))) | 
| 100 | 90, 99 | mpcom 38 | . . . . . . . . . . 11
⊢ (𝑉𝐺𝐸 → ((♯‘𝑉) = 𝑛 → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑))) | 
| 101 | 100 | imp 406 | . . . . . . . . . 10
⊢ ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → (∀𝑣∀𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑)) | 
| 102 | 88, 101 | syl5 34 | . . . . . . . . 9
⊢ ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → (𝑛 ∈ ℕ0 → 𝜑)) | 
| 103 | 102 | expcom 413 | . . . . . . . 8
⊢
((♯‘𝑉) =
𝑛 → (𝑉𝐺𝐸 → (𝑛 ∈ ℕ0 → 𝜑))) | 
| 104 | 103 | com23 86 | . . . . . . 7
⊢
((♯‘𝑉) =
𝑛 → (𝑛 ∈ ℕ0
→ (𝑉𝐺𝐸 → 𝜑))) | 
| 105 | 104 | eqcoms 2744 | . . . . . 6
⊢ (𝑛 = (♯‘𝑉) → (𝑛 ∈ ℕ0 → (𝑉𝐺𝐸 → 𝜑))) | 
| 106 | 105 | imp 406 | . . . . 5
⊢ ((𝑛 = (♯‘𝑉) ∧ 𝑛 ∈ ℕ0) → (𝑉𝐺𝐸 → 𝜑)) | 
| 107 | 106 | exlimiv 1929 | . . . 4
⊢
(∃𝑛(𝑛 = (♯‘𝑉) ∧ 𝑛 ∈ ℕ0) → (𝑉𝐺𝐸 → 𝜑)) | 
| 108 | 2, 107 | sylbi 217 | . . 3
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉𝐺𝐸 → 𝜑)) | 
| 109 | 1, 108 | syl 17 | . 2
⊢ (𝑉 ∈ Fin → (𝑉𝐺𝐸 → 𝜑)) | 
| 110 | 109 | impcom 407 | 1
⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) |