Metamath Proof Explorer

Theorem brfi1indALT

Description: Alternate proof of brfi1ind , which does not use brfi1uzind . (Contributed by Alexander van der Vekens, 7-Jan-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses brfi1ind.r ⊢ Rel 𝐺
brfi1ind.f ⊢ 𝐹 ∈ V
brfi1ind.1 ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
brfi1ind.2 ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
brfi1ind.3 ⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 )
brfi1ind.4 ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
brfi1ind.base ⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 )
brfi1ind.step ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
Assertion brfi1indALT ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ) → 𝜑 )

Proof

Step Hyp Ref Expression
1 brfi1ind.r ⊢ Rel 𝐺
2 brfi1ind.f ⊢ 𝐹 ∈ V
3 brfi1ind.1 ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
4 brfi1ind.2 ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
5 brfi1ind.3 ⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 )
6 brfi1ind.4 ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
7 brfi1ind.base ⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 )
8 brfi1ind.step ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
9 hashcl ⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
10 dfclel ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ↔ ∃ 𝑛 ( 𝑛 = ( ♯ ‘ 𝑉 ) ∧ 𝑛 ∈ ℕ0 ) )
11 eqeq2 ⊢ ( 𝑥 = 0 → ( ( ♯ ‘ 𝑣 ) = 𝑥 ↔ ( ♯ ‘ 𝑣 ) = 0 ) )
12 11 anbi2d ⊢ ( 𝑥 = 0 → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) ↔ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) ) )
13 12 imbi1d ⊢ ( 𝑥 = 0 → ( ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 ) ) )
14 13 2albidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 ) ) )
15 eqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑣 ) = 𝑥 ↔ ( ♯ ‘ 𝑣 ) = 𝑦 ) )
16 15 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) ↔ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) ) )
17 16 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) → 𝜓 ) ) )
18 17 2albidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) → 𝜓 ) ) )
19 eqeq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ♯ ‘ 𝑣 ) = 𝑥 ↔ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) )
20 19 anbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) ↔ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) )
21 20 imbi1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 𝜓 ) ) )
22 21 2albidv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 𝜓 ) ) )
23 eqeq2 ⊢ ( 𝑥 = 𝑛 → ( ( ♯ ‘ 𝑣 ) = 𝑥 ↔ ( ♯ ‘ 𝑣 ) = 𝑛 ) )
24 23 anbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) ↔ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) ) )
25 24 imbi1d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) ) )
26 25 2albidv ⊢ ( 𝑥 = 𝑛 → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑥 ) → 𝜓 ) ↔ ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) ) )
27 7 gen2 ⊢ ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 )
28 breq12 ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝑣 𝐺 𝑒 ↔ 𝑤 𝐺 𝑓 ) )
29 fveqeq2 ⊢ ( 𝑣 = 𝑤 → ( ( ♯ ‘ 𝑣 ) = 𝑦 ↔ ( ♯ ‘ 𝑤 ) = 𝑦 ) )
30 29 adantr ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( ( ♯ ‘ 𝑣 ) = 𝑦 ↔ ( ♯ ‘ 𝑤 ) = 𝑦 ) )
31 28 30 anbi12d ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) ↔ ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) ) )
32 31 4 imbi12d ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) → 𝜓 ) ↔ ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ) )
33 32 cbval2vw ⊢ ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) → 𝜓 ) ↔ ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) )
34 nn0p1gt0 ⊢ ( 𝑦 ∈ ℕ0 → 0 < ( 𝑦 + 1 ) )
35 34 adantr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 0 < ( 𝑦 + 1 ) )
36 simpr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) )
37 35 36 breqtrrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 0 < ( ♯ ‘ 𝑣 ) )
38 37 adantrl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) → 0 < ( ♯ ‘ 𝑣 ) )
39 hashgt0elex ⊢ ( ( 𝑣 ∈ V ∧ 0 < ( ♯ ‘ 𝑣 ) ) → ∃ 𝑛 𝑛 ∈ 𝑣 )
40 vex ⊢ 𝑣 ∈ V
41 simpr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) → 𝑛 ∈ 𝑣 )
42 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) → 𝑦 ∈ ℕ0 )
43 hashdifsnp1 ⊢ ( ( 𝑣 ∈ V ∧ 𝑛 ∈ 𝑣 ∧ 𝑦 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) )
44 40 41 42 43 mp3an2i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) )
45 44 imp ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 )
46 peano2nn0 ⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ0 )
47 46 ad2antrr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( 𝑦 + 1 ) ∈ ℕ0 )
48 47 ad2antlr ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → ( 𝑦 + 1 ) ∈ ℕ0 )
49 simpr ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → 𝑣 𝐺 𝑒 )
50 simplrr ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) )
51 simprlr ⊢ ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) → 𝑛 ∈ 𝑣 )
52 51 adantr ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → 𝑛 ∈ 𝑣 )
53 49 50 52 3jca ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) )
54 48 53 jca ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) )
55 40 difexi ⊢ ( 𝑣 ∖ { 𝑛 } ) ∈ V
56 breq12 ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝑤 𝐺 𝑓 ↔ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) )
57 fveqeq2 ⊢ ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) → ( ( ♯ ‘ 𝑤 ) = 𝑦 ↔ ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) )
58 57 adantr ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( ( ♯ ‘ 𝑤 ) = 𝑦 ↔ ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) )
59 56 58 anbi12d ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) ↔ ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ∧ ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) ) )
60 59 6 imbi12d ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ↔ ( ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ∧ ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) → 𝜒 ) ) )
61 60 spc2gv ⊢ ( ( ( 𝑣 ∖ { 𝑛 } ) ∈ V ∧ 𝐹 ∈ V ) → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → ( ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ∧ ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) → 𝜒 ) ) )
62 55 2 61 mp2an ⊢ ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → ( ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ∧ ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 ) → 𝜒 ) )
63 62 expdimp ⊢ ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) → ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 → 𝜒 ) )
64 63 ad2antrr ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 → 𝜒 ) )
65 54 64 8 syl6an ⊢ ( ( ( ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ∧ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) ∧ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) ∧ 𝑣 𝐺 𝑒 ) → ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 → 𝜓 ) )
66 65 exp41 ⊢ ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( 𝑣 𝐺 𝑒 → ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 → 𝜓 ) ) ) ) )
67 66 com15 ⊢ ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
68 67 com23 ⊢ ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) = 𝑦 → ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
69 45 68 mpcom ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) )
70 69 ex ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
71 70 com23 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣 ) → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
72 71 ex ⊢ ( 𝑦 ∈ ℕ0 → ( 𝑛 ∈ 𝑣 → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) ) )
73 72 com15 ⊢ ( 𝑣 𝐺 𝑒 → ( 𝑛 ∈ 𝑣 → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) ) )
74 73 imp ⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
75 5 74 mpd ⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) )
76 75 ex ⊢ ( 𝑣 𝐺 𝑒 → ( 𝑛 ∈ 𝑣 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
77 76 com4l ⊢ ( 𝑛 ∈ 𝑣 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
78 77 exlimiv ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑣 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
79 39 78 syl ⊢ ( ( 𝑣 ∈ V ∧ 0 < ( ♯ ‘ 𝑣 ) ) → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
80 79 ex ⊢ ( 𝑣 ∈ V → ( 0 < ( ♯ ‘ 𝑣 ) → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( 𝑣 𝐺 𝑒 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) ) )
81 80 com25 ⊢ ( 𝑣 ∈ V → ( 𝑣 𝐺 𝑒 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( 0 < ( ♯ ‘ 𝑣 ) → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) ) )
82 81 elv ⊢ ( 𝑣 𝐺 𝑒 → ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( 𝑦 ∈ ℕ0 → ( 0 < ( ♯ ‘ 𝑣 ) → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) ) )
83 82 imp ⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → ( 𝑦 ∈ ℕ0 → ( 0 < ( ♯ ‘ 𝑣 ) → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) ) )
84 83 impcom ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) → ( 0 < ( ♯ ‘ 𝑣 ) → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) ) )
85 38 84 mpd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) ) → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → 𝜓 ) )
86 85 impancom ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ) → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 𝜓 ) )
87 86 alrimivv ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) ) → ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 𝜓 ) )
88 87 ex ⊢ ( 𝑦 ∈ ℕ0 → ( ∀ 𝑤 ∀ 𝑓 ( ( 𝑤 𝐺 𝑓 ∧ ( ♯ ‘ 𝑤 ) = 𝑦 ) → 𝜃 ) → ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 𝜓 ) ) )
89 33 88 syl5bi ⊢ ( 𝑦 ∈ ℕ0 → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑦 ) → 𝜓 ) → ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ) → 𝜓 ) ) )
90 14 18 22 26 27 89 nn0ind ⊢ ( 𝑛 ∈ ℕ0 → ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) )
91 1 brrelex12i ⊢ ( 𝑉 𝐺 𝐸 → ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) )
92 breq12 ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝑣 𝐺 𝑒 ↔ 𝑉 𝐺 𝐸 ) )
93 fveqeq2 ⊢ ( 𝑣 = 𝑉 → ( ( ♯ ‘ 𝑣 ) = 𝑛 ↔ ( ♯ ‘ 𝑉 ) = 𝑛 ) )
94 93 adantr ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ( ♯ ‘ 𝑣 ) = 𝑛 ↔ ( ♯ ‘ 𝑉 ) = 𝑛 ) )
95 92 94 anbi12d ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) ↔ ( 𝑉 𝐺 𝐸 ∧ ( ♯ ‘ 𝑉 ) = 𝑛 ) ) )
96 95 3 imbi12d ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) ↔ ( ( 𝑉 𝐺 𝐸 ∧ ( ♯ ‘ 𝑉 ) = 𝑛 ) → 𝜑 ) ) )
97 96 spc2gv ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) → ( ( 𝑉 𝐺 𝐸 ∧ ( ♯ ‘ 𝑉 ) = 𝑛 ) → 𝜑 ) ) )
98 97 com23 ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ( 𝑉 𝐺 𝐸 ∧ ( ♯ ‘ 𝑉 ) = 𝑛 ) → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) → 𝜑 ) ) )
99 98 expd ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝑉 𝐺 𝐸 → ( ( ♯ ‘ 𝑉 ) = 𝑛 → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) → 𝜑 ) ) ) )
100 91 99 mpcom ⊢ ( 𝑉 𝐺 𝐸 → ( ( ♯ ‘ 𝑉 ) = 𝑛 → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) → 𝜑 ) ) )
101 100 imp ⊢ ( ( 𝑉 𝐺 𝐸 ∧ ( ♯ ‘ 𝑉 ) = 𝑛 ) → ( ∀ 𝑣 ∀ 𝑒 ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝑛 ) → 𝜓 ) → 𝜑 ) )
102 90 101 syl5 ⊢ ( ( 𝑉 𝐺 𝐸 ∧ ( ♯ ‘ 𝑉 ) = 𝑛 ) → ( 𝑛 ∈ ℕ0 → 𝜑 ) )
103 102 expcom ⊢ ( ( ♯ ‘ 𝑉 ) = 𝑛 → ( 𝑉 𝐺 𝐸 → ( 𝑛 ∈ ℕ0 → 𝜑 ) ) )
104 103 com23 ⊢ ( ( ♯ ‘ 𝑉 ) = 𝑛 → ( 𝑛 ∈ ℕ0 → ( 𝑉 𝐺 𝐸 → 𝜑 ) ) )
105 104 eqcoms ⊢ ( 𝑛 = ( ♯ ‘ 𝑉 ) → ( 𝑛 ∈ ℕ0 → ( 𝑉 𝐺 𝐸 → 𝜑 ) ) )
106 105 imp ⊢ ( ( 𝑛 = ( ♯ ‘ 𝑉 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑉 𝐺 𝐸 → 𝜑 ) )
107 106 exlimiv ⊢ ( ∃ 𝑛 ( 𝑛 = ( ♯ ‘ 𝑉 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑉 𝐺 𝐸 → 𝜑 ) )
108 10 107 sylbi ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( 𝑉 𝐺 𝐸 → 𝜑 ) )
109 9 108 syl ⊢ ( 𝑉 ∈ Fin → ( 𝑉 𝐺 𝐸 → 𝜑 ) )
110 109 impcom ⊢ ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ) → 𝜑 )