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

Theorem brfi1indALT 14545
Description: Alternate proof of brfi1ind 14544, which does not use brfi1uzind 14543. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
brfi1ind.r Rel 𝐺
brfi1ind.f 𝐹 ∈ V
brfi1ind.1 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝜓𝜑))
brfi1ind.2 ((𝑣 = 𝑤𝑒 = 𝑓) → (𝜓𝜃))
brfi1ind.3 ((𝑣𝐺𝑒𝑛𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹)
brfi1ind.4 ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃𝜒))
brfi1ind.base ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)
brfi1ind.step ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛𝑣)) ∧ 𝜒) → 𝜓)
Assertion
Ref Expression
brfi1indALT ((𝑉𝐺𝐸𝑉 ∈ Fin) → 𝜑)
Distinct variable groups:   𝑒,𝐸,𝑛,𝑣   𝑓,𝐹,𝑤   𝑒,𝐺,𝑓,𝑛,𝑣,𝑤,𝑦   𝑒,𝑉,𝑛,𝑣   𝜓,𝑓,𝑛,𝑤,𝑦   𝜃,𝑒,𝑛,𝑣   𝜒,𝑓,𝑤   𝜑,𝑒,𝑛,𝑣
Allowed substitution hints:   𝜑(𝑦,𝑤,𝑓)   𝜓(𝑣,𝑒)   𝜒(𝑦,𝑣,𝑒,𝑛)   𝜃(𝑦,𝑤,𝑓)   𝐸(𝑦,𝑤,𝑓)   𝐹(𝑦,𝑣,𝑒,𝑛)   𝑉(𝑦,𝑤,𝑓)

Proof of Theorem brfi1indALT
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 hashcl 14391 . . 3 (𝑉 ∈ Fin → (♯‘𝑉) ∈ ℕ0)
2 dfclel 2814 . . . 4 ((♯‘𝑉) ∈ ℕ0 ↔ ∃𝑛(𝑛 = (♯‘𝑉) ∧ 𝑛 ∈ ℕ0))
3 eqeq2 2746 . . . . . . . . . . . . . 14 (𝑥 = 0 → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = 0))
43anbi2d 630 . . . . . . . . . . . . 13 (𝑥 = 0 → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0)))
54imbi1d 341 . . . . . . . . . . . 12 (𝑥 = 0 → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)))
652albidv 1920 . . . . . . . . . . 11 (𝑥 = 0 → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)))
7 eqeq2 2746 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = 𝑦))
87anbi2d 630 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦)))
98imbi1d 341 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓)))
1092albidv 1920 . . . . . . . . . . 11 (𝑥 = 𝑦 → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓)))
11 eqeq2 2746 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + 1) → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = (𝑦 + 1)))
1211anbi2d 630 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + 1) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))))
1312imbi1d 341 . . . . . . . . . . . 12 (𝑥 = (𝑦 + 1) → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓)))
14132albidv 1920 . . . . . . . . . . 11 (𝑥 = (𝑦 + 1) → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓)))
15 eqeq2 2746 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → ((♯‘𝑣) = 𝑥 ↔ (♯‘𝑣) = 𝑛))
1615anbi2d 630 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) ↔ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛)))
1716imbi1d 341 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓)))
18172albidv 1920 . . . . . . . . . . 11 (𝑥 = 𝑛 → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑥) → 𝜓) ↔ ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓)))
19 brfi1ind.base . . . . . . . . . . . 12 ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)
2019gen2 1792 . . . . . . . . . . 11 𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)
21 breq12 5152 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑤𝑒 = 𝑓) → (𝑣𝐺𝑒𝑤𝐺𝑓))
22 fveqeq2 6915 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑤 → ((♯‘𝑣) = 𝑦 ↔ (♯‘𝑤) = 𝑦))
2322adantr 480 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑤𝑒 = 𝑓) → ((♯‘𝑣) = 𝑦 ↔ (♯‘𝑤) = 𝑦))
2421, 23anbi12d 632 . . . . . . . . . . . . . 14 ((𝑣 = 𝑤𝑒 = 𝑓) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) ↔ (𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦)))
25 brfi1ind.2 . . . . . . . . . . . . . 14 ((𝑣 = 𝑤𝑒 = 𝑓) → (𝜓𝜃))
2624, 25imbi12d 344 . . . . . . . . . . . . 13 ((𝑣 = 𝑤𝑒 = 𝑓) → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓) ↔ ((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃)))
2726cbval2vw 2036 . . . . . . . . . . . 12 (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓) ↔ ∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃))
28 nn0p1gt0 12552 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ0 → 0 < (𝑦 + 1))
2928adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0 ∧ (♯‘𝑣) = (𝑦 + 1)) → 0 < (𝑦 + 1))
30 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0 ∧ (♯‘𝑣) = (𝑦 + 1)) → (♯‘𝑣) = (𝑦 + 1))
3129, 30breqtrrd 5175 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0 ∧ (♯‘𝑣) = (𝑦 + 1)) → 0 < (♯‘𝑣))
3231adantrl 716 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))) → 0 < (♯‘𝑣))
33 hashgt0elex 14436 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ V ∧ 0 < (♯‘𝑣)) → ∃𝑛 𝑛𝑣)
34 brfi1ind.3 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣𝐺𝑒𝑛𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹)
35 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣 ∈ V
36 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℕ0𝑛𝑣) → 𝑛𝑣)
37 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℕ0𝑛𝑣) → 𝑦 ∈ ℕ0)
38 hashdifsnp1 14541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑣 ∈ V ∧ 𝑛𝑣𝑦 ∈ ℕ0) → ((♯‘𝑣) = (𝑦 + 1) → (♯‘(𝑣 ∖ {𝑛})) = 𝑦))
3935, 36, 37, 38mp3an2i 1465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℕ0𝑛𝑣) → ((♯‘𝑣) = (𝑦 + 1) → (♯‘(𝑣 ∖ {𝑛})) = 𝑦))
4039imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (♯‘(𝑣 ∖ {𝑛})) = 𝑦)
41 peano2nn0 12563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ0)
4241ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑦 + 1) ∈ ℕ0)
4342ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → (𝑦 + 1) ∈ ℕ0)
44 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → 𝑣𝐺𝑒)
45 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → (♯‘𝑣) = (𝑦 + 1))
46 simprlr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) → 𝑛𝑣)
4746adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → 𝑛𝑣)
4844, 45, 473jca 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛𝑣))
4943, 48jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → ((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛𝑣)))
5035difexi 5335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑣 ∖ {𝑛}) ∈ V
51 brfi1ind.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 𝐹 ∈ V
52 breq12 5152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝑤𝐺𝑓 ↔ (𝑣 ∖ {𝑛})𝐺𝐹))
53 fveqeq2 6915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑤 = (𝑣 ∖ {𝑛}) → ((♯‘𝑤) = 𝑦 ↔ (♯‘(𝑣 ∖ {𝑛})) = 𝑦))
5453adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ((♯‘𝑤) = 𝑦 ↔ (♯‘(𝑣 ∖ {𝑛})) = 𝑦))
5552, 54anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) ↔ ((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦)))
56 brfi1ind.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃𝜒))
5755, 56imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ↔ (((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒)))
5857spc2gv 3599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑣 ∖ {𝑛}) ∈ V ∧ 𝐹 ∈ V) → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → (((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒)))
5950, 51, 58mp2an 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → (((𝑣 ∖ {𝑛})𝐺𝐹 ∧ (♯‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒))
6059expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦𝜒))
6160ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦𝜒))
62 brfi1ind.step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛𝑣)) ∧ 𝜒) → 𝜓)
6349, 61, 62syl6an 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) ∧ (𝑣 ∖ {𝑛})𝐺𝐹) ∧ ((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1))) ∧ 𝑣𝐺𝑒) → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦𝜓))
6463exp41 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑣𝐺𝑒 → ((♯‘(𝑣 ∖ {𝑛})) = 𝑦𝜓)))))
6564com15 101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘(𝑣 ∖ {𝑛})) = 𝑦 → ((𝑣 ∖ {𝑛})𝐺𝐹 → (((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
6665com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((♯‘(𝑣 ∖ {𝑛})) = 𝑦 → (((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
6740, 66mpcom 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ℕ0𝑛𝑣) ∧ (♯‘𝑣) = (𝑦 + 1)) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))
6867ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℕ0𝑛𝑣) → ((♯‘𝑣) = (𝑦 + 1) → ((𝑣 ∖ {𝑛})𝐺𝐹 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
6968com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℕ0𝑛𝑣) → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
7069ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ0 → (𝑛𝑣 → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))))
7170com15 101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣𝐺𝑒 → (𝑛𝑣 → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))))
7271imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣𝐺𝑒𝑛𝑣) → ((𝑣 ∖ {𝑛})𝐺𝐹 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
7334, 72mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣𝐺𝑒𝑛𝑣) → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))
7473ex 412 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣𝐺𝑒 → (𝑛𝑣 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
7574com4l 92 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝑣 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
7675exlimiv 1927 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑛 𝑛𝑣 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
7733, 76syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ∈ V ∧ 0 < (♯‘𝑣)) → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
7877ex 412 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ V → (0 < (♯‘𝑣) → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (𝑣𝐺𝑒 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))))
7978com25 99 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ V → (𝑣𝐺𝑒 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (0 < (♯‘𝑣) → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))))
8079elv 3482 . . . . . . . . . . . . . . . . . 18 (𝑣𝐺𝑒 → ((♯‘𝑣) = (𝑦 + 1) → (𝑦 ∈ ℕ0 → (0 < (♯‘𝑣) → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))))
8180imp 406 . . . . . . . . . . . . . . . . 17 ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → (𝑦 ∈ ℕ0 → (0 < (♯‘𝑣) → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))))
8281impcom 407 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))) → (0 < (♯‘𝑣) → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓)))
8332, 82mpd 15 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1))) → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → 𝜓))
8483impancom 451 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0 ∧ ∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃)) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓))
8584alrimivv 1925 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0 ∧ ∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃)) → ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓))
8685ex 412 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0 → (∀𝑤𝑓((𝑤𝐺𝑓 ∧ (♯‘𝑤) = 𝑦) → 𝜃) → ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓)))
8727, 86biimtrid 242 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑦) → 𝜓) → ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1)) → 𝜓)))
886, 10, 14, 18, 20, 87nn0ind 12710 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓))
89 brfi1ind.r . . . . . . . . . . . . 13 Rel 𝐺
9089brrelex12i 5743 . . . . . . . . . . . 12 (𝑉𝐺𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
91 breq12 5152 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝑣𝐺𝑒𝑉𝐺𝐸))
92 fveqeq2 6915 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑉 → ((♯‘𝑣) = 𝑛 ↔ (♯‘𝑉) = 𝑛))
9392adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑒 = 𝐸) → ((♯‘𝑣) = 𝑛 ↔ (♯‘𝑉) = 𝑛))
9491, 93anbi12d 632 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑒 = 𝐸) → ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) ↔ (𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛)))
95 brfi1ind.1 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝜓𝜑))
9694, 95imbi12d 344 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑉𝑒 = 𝐸) → (((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) ↔ ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → 𝜑)))
9796spc2gv 3599 . . . . . . . . . . . . . 14 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → 𝜑)))
9897com23 86 . . . . . . . . . . . . 13 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑)))
9998expd 415 . . . . . . . . . . . 12 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉𝐺𝐸 → ((♯‘𝑉) = 𝑛 → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑))))
10090, 99mpcom 38 . . . . . . . . . . 11 (𝑉𝐺𝐸 → ((♯‘𝑉) = 𝑛 → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑)))
101100imp 406 . . . . . . . . . 10 ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → (∀𝑣𝑒((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝑛) → 𝜓) → 𝜑))
10288, 101syl5 34 . . . . . . . . 9 ((𝑉𝐺𝐸 ∧ (♯‘𝑉) = 𝑛) → (𝑛 ∈ ℕ0𝜑))
103102expcom 413 . . . . . . . 8 ((♯‘𝑉) = 𝑛 → (𝑉𝐺𝐸 → (𝑛 ∈ ℕ0𝜑)))
104103com23 86 . . . . . . 7 ((♯‘𝑉) = 𝑛 → (𝑛 ∈ ℕ0 → (𝑉𝐺𝐸𝜑)))
105104eqcoms 2742 . . . . . 6 (𝑛 = (♯‘𝑉) → (𝑛 ∈ ℕ0 → (𝑉𝐺𝐸𝜑)))
106105imp 406 . . . . 5 ((𝑛 = (♯‘𝑉) ∧ 𝑛 ∈ ℕ0) → (𝑉𝐺𝐸𝜑))
107106exlimiv 1927 . . . 4 (∃𝑛(𝑛 = (♯‘𝑉) ∧ 𝑛 ∈ ℕ0) → (𝑉𝐺𝐸𝜑))
1082, 107sylbi 217 . . 3 ((♯‘𝑉) ∈ ℕ0 → (𝑉𝐺𝐸𝜑))
1091, 108syl 17 . 2 (𝑉 ∈ Fin → (𝑉𝐺𝐸𝜑))
110109impcom 407 1 ((𝑉𝐺𝐸𝑉 ∈ Fin) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wex 1775  wcel 2105  Vcvv 3477  cdif 3959  {csn 4630   class class class wbr 5147  Rel wrel 5693  cfv 6562  (class class class)co 7430  Fincfn 8983  0cc0 11152  1c1 11153   + caddc 11155   < clt 11292  0cn0 12523  chash 14365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-fz 13544  df-hash 14366
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator