Metamath Proof Explorer

Theorem fi1uzind

Description: Properties of an ordered pair 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 (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses fi1uzind.f ⊒ 𝐹 ∈ V
fi1uzind.l ⊒ 𝐿 ∈ β„•0
fi1uzind.1 ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( πœ“ ↔ πœ‘ ) )
fi1uzind.2 ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( πœ“ ↔ πœƒ ) )
fi1uzind.3 ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 ∈ 𝑣 ) β†’ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 )
fi1uzind.4 ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( πœƒ ↔ πœ’ ) )
fi1uzind.base ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ 𝑣 ) = 𝐿 ) β†’ πœ“ )
fi1uzind.step ⊒ ( ( ( ( 𝑦 + 1 ) ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ πœ’ ) β†’ πœ“ )
Assertion fi1uzind ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≀ ( β™― β€˜ 𝑉 ) ) β†’ πœ‘ )

Proof

Step Hyp Ref Expression
1 fi1uzind.f ⊒ 𝐹 ∈ V
2 fi1uzind.l ⊒ 𝐿 ∈ β„•0
3 fi1uzind.1 ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( πœ“ ↔ πœ‘ ) )
4 fi1uzind.2 ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( πœ“ ↔ πœƒ ) )
5 fi1uzind.3 ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 ∈ 𝑣 ) β†’ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 )
6 fi1uzind.4 ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( πœƒ ↔ πœ’ ) )
7 fi1uzind.base ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ 𝑣 ) = 𝐿 ) β†’ πœ“ )
8 fi1uzind.step ⊒ ( ( ( ( 𝑦 + 1 ) ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ πœ’ ) β†’ πœ“ )
9 dfclel ⊒ ( ( β™― β€˜ 𝑉 ) ∈ β„•0 ↔ βˆƒ 𝑛 ( 𝑛 = ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) )
10 nn0z ⊒ ( 𝐿 ∈ β„•0 β†’ 𝐿 ∈ β„€ )
11 2 10 mp1i ⊒ ( ( ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ 𝐿 ∈ β„€ )
12 nn0z ⊒ ( 𝑛 ∈ β„•0 β†’ 𝑛 ∈ β„€ )
13 12 ad2antlr ⊒ ( ( ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ 𝑛 ∈ β„€ )
14 breq2 ⊒ ( ( β™― β€˜ 𝑉 ) = 𝑛 β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ↔ 𝐿 ≀ 𝑛 ) )
15 14 eqcoms ⊒ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ↔ 𝐿 ≀ 𝑛 ) )
16 15 biimpcd ⊒ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ 𝐿 ≀ 𝑛 ) )
17 16 adantr ⊒ ( ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ 𝐿 ≀ 𝑛 ) )
18 17 imp ⊒ ( ( ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ 𝐿 ≀ 𝑛 )
19 eqeq1 ⊒ ( π‘₯ = 𝐿 β†’ ( π‘₯ = ( β™― β€˜ 𝑣 ) ↔ 𝐿 = ( β™― β€˜ 𝑣 ) ) )
20 19 anbi2d ⊒ ( π‘₯ = 𝐿 β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) ↔ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝐿 = ( β™― β€˜ 𝑣 ) ) ) )
21 20 imbi1d ⊒ ( π‘₯ = 𝐿 β†’ ( ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝐿 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
22 21 2albidv ⊒ ( π‘₯ = 𝐿 β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝐿 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
23 eqeq1 ⊒ ( π‘₯ = 𝑦 β†’ ( π‘₯ = ( β™― β€˜ 𝑣 ) ↔ 𝑦 = ( β™― β€˜ 𝑣 ) ) )
24 23 anbi2d ⊒ ( π‘₯ = 𝑦 β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) ↔ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) ) )
25 24 imbi1d ⊒ ( π‘₯ = 𝑦 β†’ ( ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
26 25 2albidv ⊒ ( π‘₯ = 𝑦 β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
27 eqeq1 ⊒ ( π‘₯ = ( 𝑦 + 1 ) β†’ ( π‘₯ = ( β™― β€˜ 𝑣 ) ↔ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) )
28 27 anbi2d ⊒ ( π‘₯ = ( 𝑦 + 1 ) β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) ↔ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) )
29 28 imbi1d ⊒ ( π‘₯ = ( 𝑦 + 1 ) β†’ ( ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
30 29 2albidv ⊒ ( π‘₯ = ( 𝑦 + 1 ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
31 eqeq1 ⊒ ( π‘₯ = 𝑛 β†’ ( π‘₯ = ( β™― β€˜ 𝑣 ) ↔ 𝑛 = ( β™― β€˜ 𝑣 ) ) )
32 31 anbi2d ⊒ ( π‘₯ = 𝑛 β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) ↔ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) ) )
33 32 imbi1d ⊒ ( π‘₯ = 𝑛 β†’ ( ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
34 33 2albidv ⊒ ( π‘₯ = 𝑛 β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ π‘₯ = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
35 eqcom ⊒ ( 𝐿 = ( β™― β€˜ 𝑣 ) ↔ ( β™― β€˜ 𝑣 ) = 𝐿 )
36 35 7 sylan2b ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝐿 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ )
37 36 gen2 ⊒ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝐿 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ )
38 37 a1i ⊒ ( 𝐿 ∈ β„€ β†’ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝐿 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) )
39 simpl ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ 𝑣 = 𝑀 )
40 simpr ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ 𝑒 = 𝑓 )
41 40 sbceq1d ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( [ 𝑒 / 𝑏 ] 𝜌 ↔ [ 𝑓 / 𝑏 ] 𝜌 ) )
42 39 41 sbceqbid ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ↔ [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ) )
43 fveq2 ⊒ ( 𝑣 = 𝑀 β†’ ( β™― β€˜ 𝑣 ) = ( β™― β€˜ 𝑀 ) )
44 43 eqeq2d ⊒ ( 𝑣 = 𝑀 β†’ ( 𝑦 = ( β™― β€˜ 𝑣 ) ↔ 𝑦 = ( β™― β€˜ 𝑀 ) ) )
45 44 adantr ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( 𝑦 = ( β™― β€˜ 𝑣 ) ↔ 𝑦 = ( β™― β€˜ 𝑀 ) ) )
46 42 45 anbi12d ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) ↔ ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) ) )
47 46 4 imbi12d ⊒ ( ( 𝑣 = 𝑀 ∧ 𝑒 = 𝑓 ) β†’ ( ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ) )
48 47 cbval2vw ⊒ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) )
49 nn0ge0 ⊒ ( 𝐿 ∈ β„•0 β†’ 0 ≀ 𝐿 )
50 0red ⊒ ( 𝑦 ∈ β„€ β†’ 0 ∈ ℝ )
51 nn0re ⊒ ( 𝐿 ∈ β„•0 β†’ 𝐿 ∈ ℝ )
52 2 51 mp1i ⊒ ( 𝑦 ∈ β„€ β†’ 𝐿 ∈ ℝ )
53 zre ⊒ ( 𝑦 ∈ β„€ β†’ 𝑦 ∈ ℝ )
54 letr ⊒ ( ( 0 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( ( 0 ≀ 𝐿 ∧ 𝐿 ≀ 𝑦 ) β†’ 0 ≀ 𝑦 ) )
55 50 52 53 54 syl3anc ⊒ ( 𝑦 ∈ β„€ β†’ ( ( 0 ≀ 𝐿 ∧ 𝐿 ≀ 𝑦 ) β†’ 0 ≀ 𝑦 ) )
56 0nn0 ⊒ 0 ∈ β„•0
57 pm3.22 ⊒ ( ( 0 ≀ 𝑦 ∧ 𝑦 ∈ β„€ ) β†’ ( 𝑦 ∈ β„€ ∧ 0 ≀ 𝑦 ) )
58 0z ⊒ 0 ∈ β„€
59 eluz1 ⊒ ( 0 ∈ β„€ β†’ ( 𝑦 ∈ ( β„€β‰₯ β€˜ 0 ) ↔ ( 𝑦 ∈ β„€ ∧ 0 ≀ 𝑦 ) ) )
60 58 59 mp1i ⊒ ( ( 0 ≀ 𝑦 ∧ 𝑦 ∈ β„€ ) β†’ ( 𝑦 ∈ ( β„€β‰₯ β€˜ 0 ) ↔ ( 𝑦 ∈ β„€ ∧ 0 ≀ 𝑦 ) ) )
61 57 60 mpbird ⊒ ( ( 0 ≀ 𝑦 ∧ 𝑦 ∈ β„€ ) β†’ 𝑦 ∈ ( β„€β‰₯ β€˜ 0 ) )
62 eluznn0 ⊒ ( ( 0 ∈ β„•0 ∧ 𝑦 ∈ ( β„€β‰₯ β€˜ 0 ) ) β†’ 𝑦 ∈ β„•0 )
63 56 61 62 sylancr ⊒ ( ( 0 ≀ 𝑦 ∧ 𝑦 ∈ β„€ ) β†’ 𝑦 ∈ β„•0 )
64 63 ex ⊒ ( 0 ≀ 𝑦 β†’ ( 𝑦 ∈ β„€ β†’ 𝑦 ∈ β„•0 ) )
65 55 64 syl6com ⊒ ( ( 0 ≀ 𝐿 ∧ 𝐿 ≀ 𝑦 ) β†’ ( 𝑦 ∈ β„€ β†’ ( 𝑦 ∈ β„€ β†’ 𝑦 ∈ β„•0 ) ) )
66 65 ex ⊒ ( 0 ≀ 𝐿 β†’ ( 𝐿 ≀ 𝑦 β†’ ( 𝑦 ∈ β„€ β†’ ( 𝑦 ∈ β„€ β†’ 𝑦 ∈ β„•0 ) ) ) )
67 66 com14 ⊒ ( 𝑦 ∈ β„€ β†’ ( 𝐿 ≀ 𝑦 β†’ ( 𝑦 ∈ β„€ β†’ ( 0 ≀ 𝐿 β†’ 𝑦 ∈ β„•0 ) ) ) )
68 67 pm2.43a ⊒ ( 𝑦 ∈ β„€ β†’ ( 𝐿 ≀ 𝑦 β†’ ( 0 ≀ 𝐿 β†’ 𝑦 ∈ β„•0 ) ) )
69 68 imp ⊒ ( ( 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) β†’ ( 0 ≀ 𝐿 β†’ 𝑦 ∈ β„•0 ) )
70 69 com12 ⊒ ( 0 ≀ 𝐿 β†’ ( ( 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) β†’ 𝑦 ∈ β„•0 ) )
71 2 49 70 mp2b ⊒ ( ( 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) β†’ 𝑦 ∈ β„•0 )
72 71 3adant1 ⊒ ( ( 𝐿 ∈ β„€ ∧ 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) β†’ 𝑦 ∈ β„•0 )
73 eqcom ⊒ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ↔ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) )
74 nn0p1gt0 ⊒ ( 𝑦 ∈ β„•0 β†’ 0 < ( 𝑦 + 1 ) )
75 74 adantr ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ) β†’ 0 < ( 𝑦 + 1 ) )
76 simpr ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ) β†’ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) )
77 75 76 breqtrrd ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ) β†’ 0 < ( β™― β€˜ 𝑣 ) )
78 73 77 sylan2b ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ 0 < ( β™― β€˜ 𝑣 ) )
79 78 adantrl ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) β†’ 0 < ( β™― β€˜ 𝑣 ) )
80 hashgt0elex ⊒ ( ( 𝑣 ∈ V ∧ 0 < ( β™― β€˜ 𝑣 ) ) β†’ βˆƒ 𝑛 𝑛 ∈ 𝑣 )
81 vex ⊒ 𝑣 ∈ V
82 81 a1i ⊒ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) β†’ 𝑣 ∈ V )
83 simpr ⊒ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) β†’ 𝑛 ∈ 𝑣 )
84 simpl ⊒ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) β†’ 𝑦 ∈ β„•0 )
85 hashdifsnp1 ⊒ ( ( 𝑣 ∈ V ∧ 𝑛 ∈ 𝑣 ∧ 𝑦 ∈ β„•0 ) β†’ ( ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) β†’ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) )
86 73 85 biimtrid ⊒ ( ( 𝑣 ∈ V ∧ 𝑛 ∈ 𝑣 ∧ 𝑦 ∈ β„•0 ) β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) )
87 82 83 84 86 syl3anc ⊒ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) )
88 87 imp ⊒ ( ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 )
89 peano2nn0 ⊒ ( 𝑦 ∈ β„•0 β†’ ( 𝑦 + 1 ) ∈ β„•0 )
90 89 ad2antrr ⊒ ( ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( 𝑦 + 1 ) ∈ β„•0 )
91 90 ad2antlr ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ ( 𝑦 + 1 ) ∈ β„•0 )
92 simpr ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 )
93 simplrr ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) )
94 simprlr ⊒ ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) β†’ 𝑛 ∈ 𝑣 )
95 94 adantr ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ 𝑛 ∈ 𝑣 )
96 92 93 95 3jca ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ∧ 𝑛 ∈ 𝑣 ) )
97 91 96 jca ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ ( ( 𝑦 + 1 ) ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ∧ 𝑛 ∈ 𝑣 ) ) )
98 81 difexi ⊒ ( 𝑣 βˆ– { 𝑛 } ) ∈ V
99 simpl ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) )
100 simpr ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ 𝑓 = 𝐹 )
101 100 sbceq1d ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( [ 𝑓 / 𝑏 ] 𝜌 ↔ [ 𝐹 / 𝑏 ] 𝜌 ) )
102 99 101 sbceqbid ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ↔ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) )
103 eqcom ⊒ ( 𝑦 = ( β™― β€˜ 𝑀 ) ↔ ( β™― β€˜ 𝑀 ) = 𝑦 )
104 fveqeq2 ⊒ ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) β†’ ( ( β™― β€˜ 𝑀 ) = 𝑦 ↔ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) )
105 103 104 bitrid ⊒ ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) β†’ ( 𝑦 = ( β™― β€˜ 𝑀 ) ↔ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) )
106 105 adantr ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( 𝑦 = ( β™― β€˜ 𝑀 ) ↔ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) )
107 102 106 anbi12d ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) ↔ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) ) )
108 107 6 imbi12d ⊒ ( ( 𝑀 = ( 𝑣 βˆ– { 𝑛 } ) ∧ 𝑓 = 𝐹 ) β†’ ( ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ↔ ( ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) β†’ πœ’ ) ) )
109 108 spc2gv ⊒ ( ( ( 𝑣 βˆ– { 𝑛 } ) ∈ V ∧ 𝐹 ∈ V ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ ( ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) β†’ πœ’ ) ) )
110 98 1 109 mp2an ⊒ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ ( ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 ) β†’ πœ’ ) )
111 110 expdimp ⊒ ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) β†’ ( ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 β†’ πœ’ ) )
112 111 ad2antrr ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ ( ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 β†’ πœ’ ) )
113 73 3anbi2i ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ∧ 𝑛 ∈ 𝑣 ) ↔ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) )
114 113 anbi2i ⊒ ( ( ( 𝑦 + 1 ) ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ∧ 𝑛 ∈ 𝑣 ) ) ↔ ( ( 𝑦 + 1 ) ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( β™― β€˜ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) )
115 114 8 sylanb ⊒ ( ( ( ( 𝑦 + 1 ) ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ πœ’ ) β†’ πœ“ )
116 97 112 115 syl6an ⊒ ( ( ( ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ∧ [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 ) ∧ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) ∧ [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ) β†’ ( ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 β†’ πœ“ ) )
117 116 exp41 ⊒ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 β†’ πœ“ ) ) ) ) )
118 117 com15 ⊒ ( ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
119 118 com23 ⊒ ( ( β™― β€˜ ( 𝑣 βˆ– { 𝑛 } ) ) = 𝑦 β†’ ( ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
120 88 119 mpcom ⊒ ( ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) )
121 120 ex ⊒ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
122 121 com23 ⊒ ( ( 𝑦 ∈ β„•0 ∧ 𝑛 ∈ 𝑣 ) β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
123 122 ex ⊒ ( 𝑦 ∈ β„•0 β†’ ( 𝑛 ∈ 𝑣 β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) ) )
124 123 com15 ⊒ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( 𝑛 ∈ 𝑣 β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) ) )
125 124 imp ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 ∈ 𝑣 ) β†’ ( [ ( 𝑣 βˆ– { 𝑛 } ) / π‘Ž ] [ 𝐹 / 𝑏 ] 𝜌 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
126 5 125 mpd ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 ∈ 𝑣 ) β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) )
127 126 ex ⊒ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( 𝑛 ∈ 𝑣 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
128 127 com4l ⊒ ( 𝑛 ∈ 𝑣 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
129 128 exlimiv ⊒ ( βˆƒ 𝑛 𝑛 ∈ 𝑣 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
130 80 129 syl ⊒ ( ( 𝑣 ∈ V ∧ 0 < ( β™― β€˜ 𝑣 ) ) β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
131 130 ex ⊒ ( 𝑣 ∈ V β†’ ( 0 < ( β™― β€˜ 𝑣 ) β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) ) )
132 131 com25 ⊒ ( 𝑣 ∈ V β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( 0 < ( β™― β€˜ 𝑣 ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) ) )
133 132 elv ⊒ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 β†’ ( ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) β†’ ( 𝑦 ∈ β„•0 β†’ ( 0 < ( β™― β€˜ 𝑣 ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) ) )
134 133 imp ⊒ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ ( 𝑦 ∈ β„•0 β†’ ( 0 < ( β™― β€˜ 𝑣 ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) ) )
135 134 impcom ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) β†’ ( 0 < ( β™― β€˜ 𝑣 ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) ) )
136 79 135 mpd ⊒ ( ( 𝑦 ∈ β„•0 ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) )
137 72 136 sylan ⊒ ( ( ( 𝐿 ∈ β„€ ∧ 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) ∧ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ πœ“ ) )
138 137 impancom ⊒ ( ( ( 𝐿 ∈ β„€ ∧ 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) ∧ βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ) β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) )
139 138 alrimivv ⊒ ( ( ( 𝐿 ∈ β„€ ∧ 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) ∧ βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) ) β†’ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) )
140 139 ex ⊒ ( ( 𝐿 ∈ β„€ ∧ 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) β†’ ( βˆ€ 𝑀 βˆ€ 𝑓 ( ( [ 𝑀 / π‘Ž ] [ 𝑓 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑀 ) ) β†’ πœƒ ) β†’ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
141 48 140 biimtrid ⊒ ( ( 𝐿 ∈ β„€ ∧ 𝑦 ∈ β„€ ∧ 𝐿 ≀ 𝑦 ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑦 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) β†’ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ ( 𝑦 + 1 ) = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ) )
142 22 26 30 34 38 141 uzind ⊒ ( ( 𝐿 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ 𝐿 ≀ 𝑛 ) β†’ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) )
143 11 13 18 142 syl3anc ⊒ ( ( ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) )
144 sbcex ⊒ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ 𝑉 ∈ V )
145 sbccom ⊒ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ↔ [ 𝐸 / 𝑏 ] [ 𝑉 / π‘Ž ] 𝜌 )
146 sbcex ⊒ ( [ 𝐸 / 𝑏 ] [ 𝑉 / π‘Ž ] 𝜌 β†’ 𝐸 ∈ V )
147 145 146 sylbi ⊒ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ 𝐸 ∈ V )
148 144 147 jca ⊒ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) )
149 simpl ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ 𝑣 = 𝑉 )
150 simpr ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ 𝑒 = 𝐸 )
151 150 sbceq1d ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( [ 𝑒 / 𝑏 ] 𝜌 ↔ [ 𝐸 / 𝑏 ] 𝜌 ) )
152 149 151 sbceqbid ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ↔ [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ) )
153 fveq2 ⊒ ( 𝑣 = 𝑉 β†’ ( β™― β€˜ 𝑣 ) = ( β™― β€˜ 𝑉 ) )
154 153 eqeq2d ⊒ ( 𝑣 = 𝑉 β†’ ( 𝑛 = ( β™― β€˜ 𝑣 ) ↔ 𝑛 = ( β™― β€˜ 𝑉 ) ) )
155 154 adantr ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( 𝑛 = ( β™― β€˜ 𝑣 ) ↔ 𝑛 = ( β™― β€˜ 𝑉 ) ) )
156 152 155 anbi12d ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) ↔ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) ) )
157 156 3 imbi12d ⊒ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) β†’ ( ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) ↔ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ πœ‘ ) ) )
158 157 spc2gv ⊒ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) β†’ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ πœ‘ ) ) )
159 158 com23 ⊒ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) β†’ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) β†’ πœ‘ ) ) )
160 159 expd ⊒ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) β†’ πœ‘ ) ) ) )
161 148 160 mpcom ⊒ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) β†’ πœ‘ ) ) )
162 161 imp ⊒ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ ( βˆ€ 𝑣 βˆ€ 𝑒 ( ( [ 𝑣 / π‘Ž ] [ 𝑒 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑣 ) ) β†’ πœ“ ) β†’ πœ‘ ) )
163 143 162 syl5com ⊒ ( ( ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ πœ‘ ) )
164 163 exp31 ⊒ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ ( 𝑛 ∈ β„•0 β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ πœ‘ ) ) ) )
165 164 com14 ⊒ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑛 = ( β™― β€˜ 𝑉 ) ) β†’ ( 𝑛 ∈ β„•0 β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) ) )
166 165 expcom ⊒ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝑛 ∈ β„•0 β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) ) ) )
167 166 com24 ⊒ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( 𝑛 ∈ β„•0 β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) ) ) )
168 167 pm2.43i ⊒ ( 𝑛 = ( β™― β€˜ 𝑉 ) β†’ ( 𝑛 ∈ β„•0 β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) ) )
169 168 imp ⊒ ( ( 𝑛 = ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) )
170 169 exlimiv ⊒ ( βˆƒ 𝑛 ( 𝑛 = ( β™― β€˜ 𝑉 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) )
171 9 170 sylbi ⊒ ( ( β™― β€˜ 𝑉 ) ∈ β„•0 β†’ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) )
172 hashcl ⊒ ( 𝑉 ∈ Fin β†’ ( β™― β€˜ 𝑉 ) ∈ β„•0 )
173 171 172 syl11 ⊒ ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 β†’ ( 𝑉 ∈ Fin β†’ ( 𝐿 ≀ ( β™― β€˜ 𝑉 ) β†’ πœ‘ ) ) )
174 173 3imp ⊒ ( ( [ 𝑉 / π‘Ž ] [ 𝐸 / 𝑏 ] 𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≀ ( β™― β€˜ 𝑉 ) ) β†’ πœ‘ )